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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and