Re: [isabelle] I want to print axiomatization info



On 7/10/2012 2:57 AM, Lawrence Paulson wrote:
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.

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.

Regards,
GB






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