Re: Prove axiom in S5
From: A.S. (pleaseposttong_at_nospamatall)
Date: 03/01/05
- Next message: Chris Menzel: "Re: In the empty domain:"
- Previous message: Lester Zick: "Re: Existence of mathematical entities (Re: Successor Axiom: on what grounds TF?)"
- In reply to: muxol: "Re: Prove axiom in S5"
- Next in thread: muxol: "Re: Prove axiom in S5"
- Messages sorted by: [ date ] [ thread ]
Date: Tue, 01 Mar 2005 18:04:22 +0100
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)[/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)
>
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.
- Next message: Chris Menzel: "Re: In the empty domain:"
- Previous message: Lester Zick: "Re: Existence of mathematical entities (Re: Successor Axiom: on what grounds TF?)"
- In reply to: muxol: "Re: Prove axiom in S5"
- Next in thread: muxol: "Re: Prove axiom in S5"
- Messages sorted by: [ date ] [ thread ]
Relevant Pages
|
