LCM with 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)) ))

In[367]:=

Clear[f] ;

In[368]:=

Lin[F4]

Out[368]=

(∃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[369]:=

savedplay = ( "move 1"                     "L"                     ... "drop" BCK[F4, "LCM, MaterialImplication, CutRule, FontSize=18", savedplay] ;

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

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

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

\n\n

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

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

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

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

[Graphics:../HTMLFiles/index_460.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)))),  {}

⊢

{}

____________________________________________________________________

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_471.gif]

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

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

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

[Graphics:../HTMLFiles/index_475.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))))}

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)

____________________________________________________________________

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

Abelard moves: x=0

\n\n

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

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

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

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

[Graphics:../HTMLFiles/index_490.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))))}

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)} , ∀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_501.gif]

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

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

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

[Graphics:../HTMLFiles/index_505.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))))}

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), ∀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_516.gif]

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

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

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

[Graphics:../HTMLFiles/index_520.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))))}

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), ∀y.f(0)≤f(y), f(0)≤f(g(0))} , 

____________________________________________________________________

Abelard has no subformulas to choose.

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

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

\n\n

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

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

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

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

[Graphics:../HTMLFiles/index_536.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))))}

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), ∀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_547.gif]

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

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

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

[Graphics:../HTMLFiles/index_551.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))))}

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)} , ∀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_562.gif]

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

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

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

[Graphics:../HTMLFiles/index_566.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))))}

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), ∀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_577.gif]

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

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

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

[Graphics:../HTMLFiles/index_581.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))))}

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), ∀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 6 of the play.

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

\n\n

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

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

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

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

[Graphics:../HTMLFiles/index_597.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))))}

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)} , ∀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_608.gif]

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

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

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

[Graphics:../HTMLFiles/index_612.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))))}

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), ∀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_623.gif]

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

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

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

[Graphics:../HTMLFiles/index_627.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))))}

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), ∀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 1 of the play.

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

\n\n

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

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

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

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

[Graphics:../HTMLFiles/index_643.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))))

Goal of: Abelard

{} , (∃x.∀y.f(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_654.gif]

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

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

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

[Graphics:../HTMLFiles/index_658.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.(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_669.gif]

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

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

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

[Graphics:../HTMLFiles/index_673.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_684.gif]

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

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

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

[Graphics:../HTMLFiles/index_688.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_699.gif]

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

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

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

[Graphics:../HTMLFiles/index_703.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_713.gif]

This is the list of all moves of the play:

( move 1                     L                        )            move 2      ...            L            move 13                    Atom            move 14                    drop


Created by Mathematica  (November 11, 2006)