Re: [isabelle] I want to print axiomatization info
On 7/10/2012 2:57 AM, Lawrence Paulson wrote:
> 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
> very simple). Then it is enough to prove P --> Q --> R. Which
> may as well assume that P and Q are actually true while you are
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
> 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.
I'll do the easy part and show HOL's definition of disjunction to
complete the discussion.
P | Q == !R.(P-->R) --> (Q-->R) --> R
Larry, thanks for the explanation of the not-so-straightforward logic.
This archive was generated by a fusion of
Pipermail (Mailman edition) and