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

In[371]:=

Clear[f] ;

In[372]:=

f[x_] := (x - 50)^2 ; Plot[f[x], {x, 0, 100}] ;

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

In[373]:=

F16 = Impl["MP", Ex["x", "f(x)≤f(x+27)"]] ; Lin[F16]

Out[374]=

(MP∃x.f(x)≤f(x+27))

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[375]:=

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

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

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

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

\n\n

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

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

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

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

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

Goal of: Eloise

{}

⊢

{} , (MP∃x.f(x)≤f(x+27))

Goal of: Abelard

{} , (MP∃x.f(x)≤f(x+27)),  {}

⊢

{}

____________________________________________________________________

Abelard must attack the only subformula (MP∃x.f(x)≤f(x+27))

Abelard moves: Box

\n\n

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

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

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

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

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

Goal of: Eloise

{}

⊢

{(MP∃x.f(x)≤f(x+27))} , (MP∃x.f(x)≤f(x+27))

Goal of: Abelard

{(MP∃x.f(x)≤f(x+27))} , (MP∃x.f(x)≤f(x+27)),  {}

⊢

{}

____________________________________________________________________

Eloise must either attack the left, or defend the right subformula of (MP∃x.f(x)≤f(x+27))

Eloise moves: Left

\n\n

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

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

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

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

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

Goal of: Eloise

{} , MP,  {}

⊢

{(MP∃x.f(x)≤f(x+27)), (MP∃x.f(x)≤f(x+27))}

Goal of: Abelard

{(MP∃x.f(x)≤f(x+27)), (MP∃x.f(x)≤f(x+27))}

⊢

{} , MP

____________________________________________________________________

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

Abelard moves: x=0

\n\n

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

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

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

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

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

Goal of: Eloise

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

⊢

{(MP∃x.f(x)≤f(x+27)), (MP∃x.f(x)≤f(x+27))}

Goal of: Abelard

{(MP∃x.f(x)≤f(x+27)), (MP∃x.f(x)≤f(x+27))}

⊢

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

____________________________________________________________________

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

Eloise moves: y=0+27

\n\n

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

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

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

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

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

Goal of: Eloise

{MP, ∀y.f(0)≤f(y)} , f(0)≤f(0+27),  {}

⊢

{(MP∃x.f(x)≤f(x+27)), (MP∃x.f(x)≤f(x+27))}

Goal of: Abelard

{(MP∃x.f(x)≤f(x+27)), (MP∃x.f(x)≤f(x+27))}

⊢

{MP, ∀y.f(0)≤f(y)} , f(0)≤f(0+27)

____________________________________________________________________

f(0)≤f(0+27) is false.

Abelard moves: Atom

\n\n

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

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

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

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

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

Goal of: Eloise

{MP, ∀y.f(0)≤f(y), f(0)≤f(0+27)} , ,  {}

⊢

{(MP∃x.f(x)≤f(x+27)), (MP∃x.f(x)≤f(x+27))}

Goal of: Abelard

{(MP∃x.f(x)≤f(x+27)), (MP∃x.f(x)≤f(x+27))}

⊢

{MP, ∀y.f(0)≤f(y), f(0)≤f(0+27)} , 

____________________________________________________________________

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

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

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

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

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

Goal of: Eloise

{} , MP,  {}

⊢

{(MP∃x.f(x)≤f(x+27)), (MP∃x.f(x)≤f(x+27))}

Goal of: Abelard

{(MP∃x.f(x)≤f(x+27)), (MP∃x.f(x)≤f(x+27))}

⊢

{MP, ∀y.f(0)≤f(y), f(0)≤f(0+27)} , MP

____________________________________________________________________

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

Abelard moves: x=27

\n\n

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

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

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

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

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

Goal of: Eloise

{MP} , ∀y.f(27)≤f(y),  {}

⊢

{(MP∃x.f(x)≤f(x+27)), (MP∃x.f(x)≤f(x+27))}

Goal of: Abelard

{(MP∃x.f(x)≤f(x+27)), (MP∃x.f(x)≤f(x+27))}

⊢

{MP} , ∀y.f(27)≤f(y)

____________________________________________________________________

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

Eloise moves: y=27+27

\n\n

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

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

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

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

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

Goal of: Eloise

{MP, ∀y.f(27)≤f(y)} , f(27)≤f(27+27),  {}

⊢

{(MP∃x.f(x)≤f(x+27)), (MP∃x.f(x)≤f(x+27))}

Goal of: Abelard

{(MP∃x.f(x)≤f(x+27)), (MP∃x.f(x)≤f(x+27))}

⊢

{MP, ∀y.f(27)≤f(y)} , f(27)≤f(27+27)

____________________________________________________________________

f(27)≤f(27+27) is false.

Abelard moves: Atom

\n\n

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

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

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

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

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

Goal of: Eloise

{MP, ∀y.f(27)≤f(y), f(27)≤f(27+27)} , ,  {}

⊢

{(MP∃x.f(x)≤f(x+27)), (MP∃x.f(x)≤f(x+27))}

Goal of: Abelard

{(MP∃x.f(x)≤f(x+27)), (MP∃x.f(x)≤f(x+27))}

⊢

{MP, ∀y.f(27)≤f(y), f(27)≤f(27+27)} , 

____________________________________________________________________

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

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

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

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

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

Goal of: Eloise

{} , MP,  {}

⊢

{(MP∃x.f(x)≤f(x+27)), (MP∃x.f(x)≤f(x+27))}

Goal of: Abelard

{(MP∃x.f(x)≤f(x+27)), (MP∃x.f(x)≤f(x+27))}

⊢

{MP, ∀y.f(27)≤f(y), f(27)≤f(27+27)} , MP

____________________________________________________________________

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

Abelard moves: x=27+27

\n\n

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

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

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

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

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

Goal of: Eloise

{MP} , ∀y.f(27+27)≤f(y),  {}

⊢

{(MP∃x.f(x)≤f(x+27)), (MP∃x.f(x)≤f(x+27))}

Goal of: Abelard

{(MP∃x.f(x)≤f(x+27)), (MP∃x.f(x)≤f(x+27))}

⊢

{MP} , ∀y.f(27+27)≤f(y)

____________________________________________________________________

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

Eloise moves: y=27+27+27

\n\n

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

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

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

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

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

Goal of: Eloise

{MP, ∀y.f(27+27)≤f(y)} , f(27+27)≤f(27+27+27),  {}

⊢

{(MP∃x.f(x)≤f(x+27)), (MP∃x.f(x)≤f(x+27))}

Goal of: Abelard

{(MP∃x.f(x)≤f(x+27)), (MP∃x.f(x)≤f(x+27))}

⊢

{MP, ∀y.f(27+27)≤f(y)} , f(27+27)≤f(27+27+27)

____________________________________________________________________

f(27+27)≤f(27+27+27) is true.

Abelard moves: Atom

\n\n

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

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

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

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

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

Goal of: Eloise

{MP, ∀y.f(27+27)≤f(y), f(27+27)≤f(27+27+27)} , ,  {}

⊢

{(MP∃x.f(x)≤f(x+27)), (MP∃x.f(x)≤f(x+27))}

Goal of: Abelard

{(MP∃x.f(x)≤f(x+27)), (MP∃x.f(x)≤f(x+27))}

⊢

{MP, ∀y.f(27+27)≤f(y), f(27+27)≤f(27+27+27)} , 

____________________________________________________________________

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

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

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

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

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

Goal of: Eloise

{MP, ∀y.f(27+27)≤f(y), f(27+27)≤f(27+27+27), }

⊢

{(MP∃x.f(x)≤f(x+27))} , (MP∃x.f(x)≤f(x+27))

Goal of: Abelard

{(MP∃x.f(x)≤f(x+27))} , (MP∃x.f(x)≤f(x+27)),  {}

⊢

{}

____________________________________________________________________

Eloise must either attack the left, or defend the right subformula of (MP∃x.f(x)≤f(x+27))

Eloise moves: Right

\n\n

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

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

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

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

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

Goal of: Eloise

{MP, ∀y.f(27+27)≤f(y), f(27+27)≤f(27+27+27), }

⊢

{(MP∃x.f(x)≤f(x+27)), (MP∃x.f(x)≤f(x+27))} , ∃x.f(x)≤f(x+27)

Goal of: Abelard

{(MP∃x.f(x)≤f(x+27)), (MP∃x.f(x)≤f(x+27))} , ∃x.f(x)≤f(x+27),  {}

⊢

{}

____________________________________________________________________

Eloise must defend of some instance x of ∃x.f(x)≤f(x+27)

Eloise moves: x=27+27

\n\n

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

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

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

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

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

Goal of: Eloise

{MP, ∀y.f(27+27)≤f(y), f(27+27)≤f(27+27+27), }

⊢

{(MP∃x.f(x)≤f(x+27)), (MP∃x.f(x)≤f(x+27)), ∃x.f(x)≤f(x+27)} , f(27+27)≤f(27+27+27)

Goal of: Abelard

{(MP∃x.f(x)≤f(x+27)), (MP∃x.f(x)≤f(x+27)), ∃x.f(x)≤f(x+27)} , f(27+27)≤f(27+27+27),  {}

⊢

{}

____________________________________________________________________

f(27+27)≤f(27+27+27) is true.

Eloise moves: Atom

\n\n

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

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

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

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

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

Goal of: Eloise

{MP, ∀y.f(27+27)≤f(y), f(27+27)≤f(27+27+27), }

⊢

{(MP∃x.f(x)≤f(x+27)), (MP∃x.f(x)≤f(x+27)), ∃x.f(x)≤f(x+27), f(27+27)≤f(27+27+27)} , 

Goal of: Abelard

{(MP∃x.f(x)≤f(x+27)), (MP∃x.f(x)≤f(x+27)), ∃x.f(x)≤f(x+27), f(27+27)≤f(27+27+27)} , ,  {}

⊢

{}

____________________________________________________________________

Abelard has no subformulas to choose.

Abelard gives up.

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

This is the list of all moves of the play:

( move 1 Box ) move 2 L move 3 0 ... move 12 R move 13 27+27 move 14 Atom move 15 drop

In[377]:=

Clear[f] ;

Created by Mathematica  (November 11, 2006)