Re: [isabelle] I want to print axiomatization info

On 7/10/2012 2:14 AM, Lars Noschinski wrote:

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

!R. ((P /\ Q) \/ R)

This would be "!R. (~(P /\ Q) \/ R)"

I don't know. This is what I get:

(P --> Q --> R) --> R
  == ((P /\ Q) --> R) --> R)
  == (~(P /\ Q) \/ R) --> R)
  == ~(~(P /\ Q) \/ R) \/ R
  == ((P /\ Q) /\ ~R) \/ R
  == ((P /\ Q) \/ R) /\ (~R \/ R)
  == (P /\ Q) \/ R

So when R=false, the reduction above functions like conjunction. This
brings to my attention to the definition

False == (!P. P).

"!P. P" just says "all propositions hold". As long as our logic is
consistent, this is not going to be the case, so we choose this as our
value for False.

Okay, that's good to know. I'm still transitioning from truth tables, where writing a formula doesn't assert anything, at least that's how I've always viewed it for the connectives /\, \/, -->, and ~.

I did decide previously that I should interpret "!P. P" as asserting that P is always true, which helps me with it being the definition of False, but it doesn't help me understand

  !R. ((P /\ Q) \/ R), or even
  !R. (~(P /\ Q) \/ R).

The "P" and "Q" part of the "conj" (infixed as "&", and "/\") definition makes sense to me because when I use the function

  conj P Q,

in my mind, I go through the truth table and make assignments to "P" and "Q" and decide what result I should get based on how the function was being used in a statement.


  !R. ((P /\ Q) \/ R),

I try to use the same trick and say, "it's asserting that for every R, R is always true", but that doesn't work. If R is always true, then the statement is always true. But if it's always false, then the statement operates as a conjunction.

Well, okay, the above sentence shows I still have trouble interpreting things.

What I know is that saying "every proposition R is true" is a false statement, so if that's what makes R always false in the statement "((P /\ Q) \/ R)", then the statement as a whole works.

Ah, maybe I have it. The statement "!R. ((P /\ Q) \/ R)" could be asserting this:

"For every proposition R, (P /\ Q) is true or R is true."

A more friendlier statement would be this, using your statement above:

"Every proposition is true or (P /\ Q) is true".

I guess that's it. Simple stuff, unless it's not.

Thanks for the help.


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