Constructivist help, please

[and...@acooke.org]

Hi,

(This is for private study; nothing to do with any kind of
qualification or exam)

I'm trying to learn about logic; in particular constructivist logic (as
part of understanding the relationship between types in programming
languages, propositions, proofs etc). While I've managed to solve some
basic proofs, I'm having a hard time with (A u B) => -(-A n -B)

I'm assured that this can be proved without the law of the excluded
middle, but I can't see how to do so in a constructivist manner. I'd
really appreciate it if someone could help me out; when I was at
university (many years ago!) working a few examples out with a tutor
really helped...

To see the approach I'm using, the steps that are valid in a proof, and
some comments on what I think the problem may be, please see
http://www.acooke.org/cute/TTFPExerci1.html#Tue-31-Jan-2006-17-18-01-0300-CLST

I do have one kind-of proof, later in that page, but it's not a series
of "constructive" steps. I'd really like a proof similar in style to
the ones earlier in that page. For example, transitivity of
implication:

[A]1 A => B
------------ (=> E)
B B => C
---------------------------- (=> E)
C
------ (=> I1)
A => C

Thanks!
Andrew

[H. J. Sander Bruggink]

and...@acooke.org wrote:
> Hi,
>
> (This is for private study; nothing to do with any kind of
> qualification or exam)
>
> I'm trying to learn about logic; in particular constructivist logic (as
> part of understanding the relationship between types in programming
> languages, propositions, proofs etc). While I've managed to solve some
> basic proofs, I'm having a hard time with (A u B) => -(-A n -B)

Remember that ~A is shorthand for A -> F. So in order
prove ~A, you can assume A, and prove a contradiction
from that assumption.

In your case, first assume (A v B). Then assume
(~A n ~B), and after that it won't be too hard to come
to a contradiction.

groente
-- Sander

[and...@acooke.org]

Thanks, but I still don't see how to make this "work" inside the
notation. As you say, it is easy to get a contradiction, but I seem to
be left with (X n Y) => F when what I wanted was X => (Y => F).

Your argument is totally clear, but I can't see how to make the
transition above using the axioms I have:

A B A n B
----- (n I) ----- (n E)
A n B A

[A] A A => B
: --------- (=> E)
B B
------ (=> I)
A => B

A [A] [B]
----- (u I) : :
A u B A u B C C
--------------- (u E)
C

-A = A => ! (defn) !
(! is bottom) - (! E / absurdity)
A

[A] [A] A -A
: : ----- (- E)
B -B B
-------- (- I)
-A

Sorry if this is really stupid, but as I understand things it is
critical the axioms are sufficient and that the process be "mechanical".

[H. J. Sander Bruggink]

[H. J. Sander Bruggink]

(Forget the other message, I pressed send to quickly.)

and...@acooke.org wrote:
> Thanks, but I still don't see how to make this "work" inside the
> notation. As you say, it is easy to get a contradiction, but I seem to
> be left with (X n Y) => F when what I wanted was X => (Y => F).

I take it you have X = A v B and Y = ~A n ~B, in this case?

Then you should get X => (Y => F), if you followed my
instructions.

You should use the (=>I) *twice*; you don't need a
(n I) rule.

In general, in constructive logic, work on your proof from
the conclusion to the premises. Look at the main connective
of your current goal. The introduction rule for the main
connective should be the last rule you use. Now you have
one ore more new goals that you need to prove, and possibly
a few new premisses.

When your goal has no connective, then you look at the main
connectives of your current premisses, and use the
elimination rules to try to prove your goal from them.

groente
-- Sander

[and...@acooke.org]

Ah, OK, yes, it's obvious now. Sorry - I gave up too soon there (I'd
been going round in circles on my own for too long and was a bit fed
up....). Thanks for the general guidelines (which is the kind of thing
I was really trying to get out of this).

Thanks again,
Andrew