# 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.
```
With

!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.

Regards,
GB

```

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