Intuitionistic Logic with Cut rule: rational numbers are dense.
∀x.∀y.(x<y⇒∃z.(x<z∧z<y))

In[356]:=

F8 = Un["x", Un["y", Impl["x<y", Ex["z", Conj["x<z", "z<y"]]]]] ; Lin[F8]

Out[357]=

∀x.∀y.(x<y∃z.(x<z∧z<y))

Abelard uses backtracking to check twice the claims of Eloise. This is a non-essential use of backtracking by Abelard. We choose the parameter of the game.

In[358]:=

savedplay =  ( "move 1" "0" ) ; ... stic, ConstructiveImplication, CutRule", "TreeWidth=800,FontSize=18", savedplay] ;

[Graphics:../HTMLFiles/index_5.gif]

[Graphics:../HTMLFiles/index_6.gif]

[Graphics:../HTMLFiles/index_7.gif]

\n\n

[Graphics:../HTMLFiles/index_9.gif]

[Graphics:../HTMLFiles/index_10.gif]

[Graphics:../HTMLFiles/index_11.gif]

[Graphics:../HTMLFiles/index_12.gif]

[Graphics:../HTMLFiles/index_13.gif]

Goal of: Eloise

{}

⊢

∀x.∀y.(x<y∃z.(x<z∧z<y))

Goal of: Abelard

{} , ∀x.∀y.(x<y∃z.(x<z∧z<y)),  {}

⊢

{}

____________________________________________________________________

Abelard must attack some instance x of ∀x.∀y.(x<y∃z.(x<z∧z<y))

Abelard moves: x=0

\n\n

[Graphics:../HTMLFiles/index_24.gif]

[Graphics:../HTMLFiles/index_25.gif]

[Graphics:../HTMLFiles/index_26.gif]

[Graphics:../HTMLFiles/index_27.gif]

[Graphics:../HTMLFiles/index_28.gif]

Goal of: Eloise

{}

⊢

∀y.(0<y∃z.(0<z∧z<y))

Goal of: Abelard

{∀x.∀y.(x<y∃z.(x<z∧z<y))} , ∀y.(0<y∃z.(0<z∧z<y)),  {}

⊢

{}

____________________________________________________________________

Abelard must attack some instance y of ∀y.(0<y∃z.(0<z∧z<y))

Abelard moves: y=1

\n\n

[Graphics:../HTMLFiles/index_39.gif]

[Graphics:../HTMLFiles/index_40.gif]

[Graphics:../HTMLFiles/index_41.gif]

[Graphics:../HTMLFiles/index_42.gif]

[Graphics:../HTMLFiles/index_43.gif]

Goal of: Eloise

{}

⊢

(0<1∃z.(0<z∧z<1))

Goal of: Abelard

{∀x.∀y.(x<y∃z.(x<z∧z<y)), ∀y.(0<y ... 43;z<y))} , (0<1∃z.(0<z∧z<1)),  {}

⊢

{}

____________________________________________________________________

Abelard must attack the only subformula (0<1∃z.(0<z∧z<1))

Abelard moves: Box

\n\n

[Graphics:../HTMLFiles/index_54.gif]

[Graphics:../HTMLFiles/index_55.gif]

[Graphics:../HTMLFiles/index_56.gif]

[Graphics:../HTMLFiles/index_57.gif]

[Graphics:../HTMLFiles/index_58.gif]

Goal of: Eloise

{}

⊢

(0<1∃z.(0<z∧z<1))

Goal of: Abelard

{∀x.∀y.(x<y∃z.(x<z∧z<y)), ∀y.(0<y ... 43;z<1))} , (0<1∃z.(0<z∧z<1)),  {}

⊢

{}

____________________________________________________________________

Eloise must either attack the left, or defend the right subformula of (0<1∃z.(0<z∧z<1))

Eloise moves: Right

\n\n

[Graphics:../HTMLFiles/index_69.gif]

[Graphics:../HTMLFiles/index_70.gif]

[Graphics:../HTMLFiles/index_71.gif]

[Graphics:../HTMLFiles/index_72.gif]

[Graphics:../HTMLFiles/index_73.gif]

Goal of: Eloise

{}

⊢

∃z.(0<z∧z<1)

Goal of: Abelard

{∀x.∀y.(x<y∃z.(x<z∧z<y)), ∀y.(0<y ... 07;z.(0<z∧z<1))} , ∃z.(0<z∧z<1),  {}

⊢

{}

____________________________________________________________________

Eloise must defend of some instance z of ∃z.(0<z∧z<1)

Eloise moves: z=1/2

\n\n

[Graphics:../HTMLFiles/index_84.gif]

[Graphics:../HTMLFiles/index_85.gif]

[Graphics:../HTMLFiles/index_86.gif]

[Graphics:../HTMLFiles/index_87.gif]

[Graphics:../HTMLFiles/index_88.gif]

Goal of: Eloise

{}

⊢

(0<1/2∧1/2<1)

Goal of: Abelard

{∀x.∀y.(x<y∃z.(x<z∧z<y)), ∀y.(0<y ... , ∃z.(0<z∧z<1)} , (0<1/2∧1/2<1),  {}

⊢

{}

____________________________________________________________________

Abelard must attack the left or right subformula of (0<1/2∧1/2<1)

Abelard moves: Left

\n\n

[Graphics:../HTMLFiles/index_99.gif]

[Graphics:../HTMLFiles/index_100.gif]

[Graphics:../HTMLFiles/index_101.gif]

[Graphics:../HTMLFiles/index_102.gif]

[Graphics:../HTMLFiles/index_103.gif]

Goal of: Eloise

{}

⊢

0<1/2

Goal of: Abelard

{∀x.∀y.(x<y∃z.(x<z∧z<y)), ∀y.(0<y ... .(0<z∧z<1), (0<1/2∧1/2<1)} , 0<1/2,  {}

⊢

{}

____________________________________________________________________

0<1/2 is true.

Eloise moves: Atom

\n\n

[Graphics:../HTMLFiles/index_114.gif]

[Graphics:../HTMLFiles/index_115.gif]

[Graphics:../HTMLFiles/index_116.gif]

[Graphics:../HTMLFiles/index_117.gif]

[Graphics:../HTMLFiles/index_118.gif]

Goal of: Eloise

{}

⊢



Goal of: Abelard

{∀x.∀y.(x<y∃z.(x<z∧z<y)), ∀y.(0<y ... 8743;z<1), (0<1/2∧1/2<1), 0<1/2} , ,  {}

⊢

{}

____________________________________________________________________

Abelard has no subformulas to choose.

Abelard backtracks to the node number 6 of the play.

This backtracking re-uses an hypothesis or defends the current goal (intuitionistic move).

\n\n

[Graphics:../HTMLFiles/index_130.gif]

[Graphics:../HTMLFiles/index_131.gif]

[Graphics:../HTMLFiles/index_132.gif]

[Graphics:../HTMLFiles/index_133.gif]

[Graphics:../HTMLFiles/index_134.gif]

Goal of: Eloise

{}

⊢

(0<1/2∧1/2<1)

Goal of: Abelard

{∀x.∀y.(x<y∃z.(x<z∧z<y)), ∀y.(0<y ... ∧z<1)} , (0<1/2∧1/2<1),  {0<1/2, }

⊢

{}

____________________________________________________________________

Abelard must attack the left or right subformula of (0<1/2∧1/2<1)

Abelard moves: Right

\n\n

[Graphics:../HTMLFiles/index_145.gif]

[Graphics:../HTMLFiles/index_146.gif]

[Graphics:../HTMLFiles/index_147.gif]

[Graphics:../HTMLFiles/index_148.gif]

[Graphics:../HTMLFiles/index_149.gif]

Goal of: Eloise

{}

⊢

1/2<1

Goal of: Abelard

{∀x.∀y.(x<y∃z.(x<z∧z<y)), ∀y.(0<y ... 1), (0<1/2∧1/2<1), 0<1/2, } , 1/2<1,  {}

⊢

{}

____________________________________________________________________

1/2<1 is true.

Eloise moves: Atom

\n\n

[Graphics:../HTMLFiles/index_160.gif]

[Graphics:../HTMLFiles/index_161.gif]

[Graphics:../HTMLFiles/index_162.gif]

[Graphics:../HTMLFiles/index_163.gif]

[Graphics:../HTMLFiles/index_164.gif]

Goal of: Eloise

{}

⊢



Goal of: Abelard

{∀x.∀y.(x<y∃z.(x<z∧z<y)), ∀y.(0<y ... 1/2∧1/2<1), 0<1/2, , 1/2<1} , ,  {}

⊢

{}

____________________________________________________________________

Abelard has no subformulas to choose.

Abelard gives up.

[Graphics:../HTMLFiles/index_174.gif]

This is the list of all moves of the play:

( move 1 0 ) move 2 1 move 3 Box ... move 8 bck 6 move 8 R move 9 Atom move 10 drop

Created by Mathematica  (November 11, 2006)