LCM with Constructive Implication and Cut rule: using Minimum Principle, prove that the system f(x)≤f(g(x))∧f(x)≤f(h(x)) has a solution.
A Cut between: ∃x.∀y.f(x)≤f(y) and (∃x.∀y.f(x)≤f(y) ⇒ ∃x.(  f(x)≤f(g(x))  ∧  f(x)≤f(h(x)) ))

We choose the parameters of the game. All moves by Eloise are considered intuitionistic. Backtracking used by Eloise corresponds to (re)use of input, and does not modofy the output.

In[378]:=

Clear[f] ;

In[379]:=

Lin[F4]

Out[379]=

(∃x.∀y.f(x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x))))

We choose the parameters of the game.

In[380]:=

savedplay = ( "move 1" "Box" ... t;drop" BCK[F4, "LCM, ConstructiveImplication, CutRule, FontSize=18", savedplay] ;

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

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

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

\n\n

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

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

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

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

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

Goal of: Eloise

{}

⊢

{} , (∃x.∀y.f(x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x))))

Goal of: Abelard

{} , (∃x.∀y.f(x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x)))),  {}

⊢

{}

____________________________________________________________________

Abelard must attack the only subformula (∃x.∀y.f(x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x))))

Abelard moves: Box

\n\n

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

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

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

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

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

Goal of: Eloise

{}

⊢

{(∃x.∀y.f(x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x ... ;(∃x.∀y.f(x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x))))

Goal of: Abelard

{(∃x.∀y.f(x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x ... (x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x)))),  {}

⊢

{}

____________________________________________________________________

Eloise must either attack the left, or defend the right subformula of (∃x.∀y.f(x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x))))

Eloise moves: Left

\n\n

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

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

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

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

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

Goal of: Eloise

{} , ∃x.∀y.f(x)≤f(y),  {}

⊢

{(∃x.∀y.f(x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x ... (∃x.∀y.f(x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x))))}

Goal of: Abelard

{(∃x.∀y.f(x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x ... (∃x.∀y.f(x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x))))}

⊢

{} , ∃x.∀y.f(x)≤f(y)

____________________________________________________________________

Abelard must defend of some instance x of ∃x.∀y.f(x)≤f(y)

Abelard moves: x=0

\n\n

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

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

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

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

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

Goal of: Eloise

{∃x.∀y.f(x)≤f(y)} , ∀y.f(0)≤f(y),  {}

⊢

{(∃x.∀y.f(x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x ... (∃x.∀y.f(x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x))))}

Goal of: Abelard

{(∃x.∀y.f(x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x ... (∃x.∀y.f(x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x))))}

⊢

{∃x.∀y.f(x)≤f(y)} , ∀y.f(0)≤f(y)

____________________________________________________________________

Eloise must attack some instance y of ∀y.f(0)≤f(y)

Eloise moves: y=g(0)

\n\n

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

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

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

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

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

Goal of: Eloise

{∃x.∀y.f(x)≤f(y), ∀y.f(0)≤f(y)} , f(0)≤f(g(0)),  {}

⊢

{(∃x.∀y.f(x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x ... (∃x.∀y.f(x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x))))}

Goal of: Abelard

{(∃x.∀y.f(x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x ... (∃x.∀y.f(x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x))))}

⊢

{∃x.∀y.f(x)≤f(y), ∀y.f(0)≤f(y)} , f(0)≤f(g(0))

____________________________________________________________________

f(0)≤f(g(0)) is false.

Abelard moves: Atom

\n\n

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

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

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

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

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

Goal of: Eloise

{∃x.∀y.f(x)≤f(y), ∀y.f(0)≤f(y), f(0)≤f(g(0))} , ,  {}

⊢

{(∃x.∀y.f(x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x ... (∃x.∀y.f(x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x))))}

Goal of: Abelard

{(∃x.∀y.f(x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x ... (∃x.∀y.f(x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x))))}

⊢

{∃x.∀y.f(x)≤f(y), ∀y.f(0)≤f(y), f(0)≤f(g(0))} , 

____________________________________________________________________

Abelard has no subformulas to choose.

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

This backtracking drops out the current goal and possibly more nodes (proper LCM move).

\n\n

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

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

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

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

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

Goal of: Eloise

{} , ∃x.∀y.f(x)≤f(y),  {}

⊢

{(∃x.∀y.f(x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x ... (∃x.∀y.f(x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x))))}

Goal of: Abelard

{(∃x.∀y.f(x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x ... (∃x.∀y.f(x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x))))}

⊢

{∃x.∀y.f(x)≤f(y), ∀y.f(0)≤f(y), f(0)≤f(g(0))} , ∃x.∀y.f(x)≤f(y)

____________________________________________________________________

Abelard must defend of some instance x of ∃x.∀y.f(x)≤f(y)

Abelard moves: x=g(0)

\n\n

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

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

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

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

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

Goal of: Eloise

{∃x.∀y.f(x)≤f(y)} , ∀y.f(g(0))≤f(y),  {}

⊢

{(∃x.∀y.f(x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x ... (∃x.∀y.f(x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x))))}

Goal of: Abelard

{(∃x.∀y.f(x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x ... (∃x.∀y.f(x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x))))}

⊢

{∃x.∀y.f(x)≤f(y)} , ∀y.f(g(0))≤f(y)

____________________________________________________________________

Eloise must attack some instance y of ∀y.f(g(0))≤f(y)

Eloise moves: y=g(g(0))

\n\n

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

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

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

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

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

Goal of: Eloise

{∃x.∀y.f(x)≤f(y), ∀y.f(g(0))≤f(y)} , f(g(0))≤f(g(g(0))),  {}

⊢

{(∃x.∀y.f(x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x ... (∃x.∀y.f(x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x))))}

Goal of: Abelard

{(∃x.∀y.f(x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x ... (∃x.∀y.f(x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x))))}

⊢

{∃x.∀y.f(x)≤f(y), ∀y.f(g(0))≤f(y)} , f(g(0))≤f(g(g(0)))

____________________________________________________________________

f(g(0))≤f(g(g(0))) is true.

Abelard moves: Atom

\n\n

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

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

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

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

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

Goal of: Eloise

{∃x.∀y.f(x)≤f(y), ∀y.f(g(0))≤f(y), f(g(0))≤f(g(g(0)))} , ,  {}

⊢

{(∃x.∀y.f(x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x ... (∃x.∀y.f(x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x))))}

Goal of: Abelard

{(∃x.∀y.f(x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x ... (∃x.∀y.f(x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x))))}

⊢

{∃x.∀y.f(x)≤f(y), ∀y.f(g(0))≤f(y), f(g(0))≤f(g(g(0)))} , 

____________________________________________________________________

Eloise has no subformulas to choose.

Eloise backtracks to the node number 7 of the play.

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

\n\n

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

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

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

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

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

Goal of: Eloise

{∃x.∀y.f(x)≤f(y)} , ∀y.f(g(0))≤f(y),  {f(g(0))≤f(g(g(0))), }

⊢

{(∃x.∀y.f(x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x ... (∃x.∀y.f(x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x))))}

Goal of: Abelard

{(∃x.∀y.f(x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x ... (∃x.∀y.f(x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x))))}

⊢

{∃x.∀y.f(x)≤f(y)} , ∀y.f(g(0))≤f(y)

____________________________________________________________________

Eloise must attack some instance y of ∀y.f(g(0))≤f(y)

Eloise moves: y=h(g(0))

\n\n

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

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

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

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

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

Goal of: Eloise

{∃x.∀y.f(x)≤f(y), ∀y.f(g(0))≤f(y), f(g(0))≤f(g(g(0))), } , f(g(0))≤f(h(g(0))),  {}

⊢

{(∃x.∀y.f(x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x ... (∃x.∀y.f(x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x))))}

Goal of: Abelard

{(∃x.∀y.f(x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x ... (∃x.∀y.f(x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x))))}

⊢

{∃x.∀y.f(x)≤f(y), ∀y.f(g(0))≤f(y)} , f(g(0))≤f(h(g(0)))

____________________________________________________________________

f(g(0))≤f(h(g(0))) is true.

Abelard moves: Atom

\n\n

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

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

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

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

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

Goal of: Eloise

{∃x.∀y.f(x)≤f(y), ∀y.f(g(0))≤f(y), f(g(0))≤f(g(g(0))), , f(g(0))≤f(h(g(0)))} , ,  {}

⊢

{(∃x.∀y.f(x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x ... (∃x.∀y.f(x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x))))}

Goal of: Abelard

{(∃x.∀y.f(x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x ... (∃x.∀y.f(x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x))))}

⊢

{∃x.∀y.f(x)≤f(y), ∀y.f(g(0))≤f(y), f(g(0))≤f(h(g(0)))} , 

____________________________________________________________________

Eloise has no subformulas to choose.

Eloise backtracks to the node number 2 of the play.

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

\n\n

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

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

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

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

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

Goal of: Eloise

{∃x.∀y.f(x)≤f(y), ∀y.f(g(0))≤f(y), f(g(0))≤f(g(g(0))), , f(g(0))≤f(h(g(0))), }

⊢

{(∃x.∀y.f(x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x ... ;(∃x.∀y.f(x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x))))

Goal of: Abelard

{(∃x.∀y.f(x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x ... (x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x)))),  {}

⊢

{}

____________________________________________________________________

Eloise must either attack the left, or defend the right subformula of (∃x.∀y.f(x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x))))

Eloise moves: Right

\n\n

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

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

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

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

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

Goal of: Eloise

{∃x.∀y.f(x)≤f(y), ∀y.f(g(0))≤f(y), f(g(0))≤f(g(g(0))), , f(g(0))≤f(h(g(0))), }

⊢

{(∃x.∀y.f(x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x ... 743;f(x)≤f(h(x))))} , ∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x)))

Goal of: Abelard

{(∃x.∀y.f(x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x ... )))} , ∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x))),  {}

⊢

{}

____________________________________________________________________

Eloise must defend of some instance x of ∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x)))

Eloise moves: x=g(0)

\n\n

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

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

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

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

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

Goal of: Eloise

{∃x.∀y.f(x)≤f(y), ∀y.f(g(0))≤f(y), f(g(0))≤f(g(g(0))), , f(g(0))≤f(h(g(0))), }

⊢

{(∃x.∀y.f(x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x ... 3;f(x)≤f(h(x)))} , (f(g(0))≤f(g(g(0)))∧f(g(0))≤f(h(g(0))))

Goal of: Abelard

{(∃x.∀y.f(x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x ... } , (f(g(0))≤f(g(g(0)))∧f(g(0))≤f(h(g(0)))),  {}

⊢

{}

____________________________________________________________________

Abelard must attack the left or right subformula of (f(g(0))≤f(g(g(0)))∧f(g(0))≤f(h(g(0))))

Abelard moves: Left

\n\n

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

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

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

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

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

Goal of: Eloise

{∃x.∀y.f(x)≤f(y), ∀y.f(g(0))≤f(y), f(g(0))≤f(g(g(0))), , f(g(0))≤f(h(g(0))), }

⊢

{(∃x.∀y.f(x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x ... g(0))≤f(g(g(0)))∧f(g(0))≤f(h(g(0))))} , f(g(0))≤f(g(g(0)))

Goal of: Abelard

{(∃x.∀y.f(x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x ... )∧f(g(0))≤f(h(g(0))))} , f(g(0))≤f(g(g(0))),  {}

⊢

{}

____________________________________________________________________

f(g(0))≤f(g(g(0))) is true.

Eloise moves: Atom

\n\n

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

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

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

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

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

Goal of: Eloise

{∃x.∀y.f(x)≤f(y), ∀y.f(g(0))≤f(y), f(g(0))≤f(g(g(0))), , f(g(0))≤f(h(g(0))), }

⊢

{(∃x.∀y.f(x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x ... 4;f(g(g(0)))∧f(g(0))≤f(h(g(0)))), f(g(0))≤f(g(g(0)))} , 

Goal of: Abelard

{(∃x.∀y.f(x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x ... g(0))≤f(h(g(0)))), f(g(0))≤f(g(g(0)))} , ,  {}

⊢

{}

____________________________________________________________________

Abelard has no subformulas to choose.

Abelard gives up.

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

This is the list of all moves of the play:

( move 1 Box ) move 2 ... L move 14 Atom move 15 drop

Created by Mathematica  (November 11, 2006)