Re: [isabelle] I want to print axiomatization info



On 10 Jul 2012, at 01:42, Gottfried Barrow wrote:

> So I reduce (!R. ((P --> Q --> R) --> R)) down to
> 
>    !R. ((P /\ Q) \/ R)

No need even to do that. The reasoning is very simple. let P and Q be two given formulas, and suppose that you have !R. ((P --> Q --> R) --> R). And suppose that you want to prove some formula, R say (just to keep things very simple). Then it is enough to prove P --> Q --> R. Which means, you may as well assume that P and Q are actually true while you are proving R. And that is what it means to know P&Q.

Disjunction can be defined similarly. If I'm not mistaken, this discovery is due to Frege.

Larry Paulson







This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.