[FOM] Some informative questions about intuitionistic logic and mathematics

[Neil Tennant]

On Mon, 7 Nov 2005, Thomas Forster wrote:

> On the subject of intuitionists not denying bivalence ...

But they can and do. An intuitionist can assert "it is not the case that
every statement is either true or false" without being committed to the
(strictly classical) conclusion "some statement is neither true nor
false". Indeed (as pointed out by Mark van Atten, the intuitionist will
also assert "no statement is neither true nor false".

> ... it may be worth noting that 
> constructive propositional logic explicitly denies that there are 
> more than two truth values.  The sequent
> 
> 
> -(A <--> B), -(B <--> C), -(C <--> A) |-
> 
> (which says roughly that A, B and C cannot all have different truth-values)
> 
> is constructively correct..... but hard! It's guaranteed to 
> keep even quite good students out of mischief for several hours

Actually, 33 milliseconds---see below ... I called your problem "thomas"
and fed it to my least talented student.

Neil Tennant

____________________________________________________________________

Script started on Tue Nov 08 18:45:10 2005
NU-Prolog 1.6.5
1?- [irf].
Loading /n/mercutio/0/neilt/prooffinders/irf.no.
Consulting /n/mercutio/0/neilt/prooffinders/irpp.nl.
Consulting /n/mercutio/0/neilt/prooffinders/irfmanager.nl.
Warning in op(1200, xfx, (?-)) -- changing a system-defined operator.
Loading /n/mercutio/0/nuprolog/lib/lib.10605/osets.no.
Consulting /n/mercutio/0/neilt/prooffinders/syntax.nl.
Consulting /n/mercutio/0/neilt/prooffinders/writeproblem.nl.
done
true.
2?- t(thomas).

PROBLEM NUMBER 1:

[not(and(if(a, b), if(b, a))), 
 not(and(if(a, c), if(c, a))), 
 not(and(if(b, c), if(c, b)))] ?- # .


The length of this problem is 25

I take only 33 ms to find the following PROOF in IR,

which has 43 steps of inference:


  |   |   |   |   |   |   |   | >i| b
  |   |   |   |   |   |   |   | >cb
  |   |   |   |   |   |   |   | >i| c
  |   |   |   |   |   |   | &i| >bc
  |   |   |   |   |   |   | &>bc>cb
  |   |   |   |   |   | ~e| ~&>bc>cb
  |   |   |   |   | >i| #
  |   |   |   |   | >ca
  |   |   |   |   |   |   |   | >i| a
  |   |   |   |   |   |   |   | >ba
  |   |   |   |   |   |   |   | >i| b
  |   |   |   |   |   |   | &i| >ab
  |   |   |   |   |   |   | &>ab>ba
  |   |   |   |   |   | ~e| ~&>ab>ba
  |   |   |   |   | >i| #
  |   |   |   | &i| >ac
  |   |   |   | &>ac>ca
  |   |   | ~e| ~&>ac>ca
  |   | >i| #
  |   | >ba
  |   |   |   |   |   |   |   | >i| a
  |   |   |   |   |   |   |   | >ca
  |   |   |   |   |   |   |   | >i| c
  |   |   |   |   |   |   | &i| >ac
  |   |   |   |   |   |   | &>ac>ca
  |   |   |   |   |   | ~e| ~&>ac>ca
  |   |   |   |   | >i| #
  |   |   |   |   | >cb
  |   |   |   |   |   |   |   | >i| a
  |   |   |   |   |   |   |   | >ba
  |   |   |   |   |   |   |   | >i| b
  |   |   |   |   |   |   | &i| >ab
  |   |   |   |   |   |   | &>ab>ba
  |   |   |   |   |   | ~e| ~&>ab>ba
  |   |   |   |   | >i| #
  |   |   |   | &i| >bc
  |   |   |   | &>bc>cb
  |   |   | ~e| ~&>bc>cb
  |   | >i| #
  | &i| >ab
  | &>ab>ba
~e| ~&>ab>ba
#


where all the given premisses have been used

and the conclusion is what was sought

Total worktime spent so far finding     1 proofs is             33      ms
Total worktime spent so far reaching    0 rejections is         0       ms
Total worktime so far on                1 problems is           33      ms


Thank you for your attention.

true.
3?- ^DEnd of Session
%       Time was    0.434s
mercutio:~/prooffinders [2] exit
script done on Tue Nov 08 18:45:30 2005