Re: Prove axiom in S5

From: A.S. (pleaseposttong_at_nospamatall)
Date: 03/02/05 

Date: Wed, 02 Mar 2005 19:03:45 +0100

On 1 Mar 2005 17:34:38 -0600,
-knowledge-@excite-dot-com.no-spam.invalid (muxol) wrote:

>> A.S.wrote:
>On 28 Feb 2005 21:34:41 -0600,
>> -knowledge-@excite-dot-com.no-spam.invalid (muxol) wrote:
>>
>> A.S.wrote:
>> Does anybody know how to prove the following using Natural
>Deduction
>> in S5 (using [] for the box, and <> for the diamond)?
>>
>> ([]A -> A), (A -> []<>A), ([]A -> [][]A) [single
>> turnstile, S5] (<>A
>> -> []<>A)<>A)<>A)<>A)[/quote:6d1a1426b3]
>
>1. A -> []<>A (axiom)
>2. <>A -> []<><>A (sub instance of 1 with
>A as the A)
>3. <><>A -> <>A (alternative axiom of []A -
>[][]A -- see end note)
>4. <><>A -> []<><>A (2,3 by
>truth-functions)
>5. <>A -> []<>A (4 with the A as the <>A)
>
>[/quote:49955b0483]
>OK, I see what you mean. But haven't you just shown that <>A
>-> []<>A
>follows from two of the axioms, I mentioned, and not all three? Your
>proof shows that (A -> []<>A), ([]A -> [][]A) |-
>(<>A -> []<>A).
>But I also wanted ([]A -> A) to figure.
>
>Or maybe I'm wrong?
>
>> Note:
>>
>> 1. []A ->[][]A
>> 2. ~[][]A -> ~[]A (1 by truth-functions (contrapositive))
>> 3. <>~[]A -> <>~A (2)
>> 4. <><>~A -> <>~A (3)
>> 5. <><>A -> <>A (4)
>>
>> QED.
>>
>>
>> Posted Via Usenet.com Premium Usenet Newsgroup Services
>> ----------------------------------------------------------
>> ** SPEED ** RETENTION ** COMPLETION ** ANONYMITY **
>> ----------------------------------------------------------
>> http://www.usenet.com
>>
>
>
>//A.S.[/quote:49955b0483]
>
>Why would you need T to figure in the proof? You don't need it. I'm
>sure you could work it in as a line of derivation somewhere, but
>why?
>

I know, but it would be nice to be able to demonstrate to some of my
fellow students that what happens, if we include T, B and S4, is that
S5 ensues. Just to display the relationship between these systems.

>Also your proof needn't consist of assumption formulas since <>A
>->[]<>A is provable strictly from axioms and transformation
>rules.

That sounds nice...

>
>
> Posted Via Usenet.com Premium Usenet Newsgroup Services
>----------------------------------------------------------
> ** SPEED ** RETENTION ** COMPLETION ** ANONYMITY **
>----------------------------------------------------------
> http://www.usenet.com

//A.S.

Relevant Pages

  • Re: DataGridPaging
    ... I want to limit the number of blogs that are ... > so if there are less than 5 than only that amount will display. ... > Posted Via Usenet.com Premium Usenet Newsgroup Services ...
    (microsoft.public.dotnet.framework.aspnet)
  • re:Set dropdownlist value
    ... The display on the screen is still "None". ... Tom. ... Posted Via Usenet.com Premium Usenet Newsgroup Services ...
    (microsoft.public.dotnet.framework.aspnet)
  • How do you get path and filename from a SaveFileDialog ?
    ... I want to get the file name and path from a SaveFileDialog (for a ... I want to display the new file name and path in the Form.text Title. ... Posted Via Usenet.com Premium Usenet Newsgroup Services ...
    (microsoft.public.dotnet.languages.csharp)
  • re:Fastest way to search through txt file?
    ... thank you but I don't need to count, I need to find a word and display ... the line in which it occured in my listbox. ... Posted Via Usenet.com Premium Usenet Newsgroup Services ...
    (microsoft.public.dotnet.languages.vb)
  • Re: Prove axiom in S5
    ... >Does anybody know how to prove the following using Natural Deduction ... follows from two of the axioms, I mentioned, and not all three? ... > Posted Via Usenet.com Premium Usenet Newsgroup Services ...
    (sci.logic)
Quantcast