Evaluating Model Classes

Mix.install([
  {:shot_tx, path: Path.join(__DIR__, "..")},
  {:kino, "~> 0.19.0"},
  {:kino_atp_client, "~> 0.1.3"}
])

Setup

import ShotTx.Prover
import ShotDs.Hol.Sigils
alias ShotDs.Tptp

defmodule Util do
  def render res do
    case res do
      {:thm, proof} ->
        frame = Kino.Frame.new()
        Kino.render(frame)
        diagram = proof |> ShotTx.Proof.to_mermaid |> Kino.Mermaid.new
        Kino.Frame.render frame, diagram
      other -> other
    end
  end
end

import Util

leibniz1 = """
thf(leibniz_t, type, l: A > A > $o).
thf(leibniz_def, definition,
  l = ^[X, Y]: ![P]: P @ X => P @ Y
).
"""

leibniz2 = """
thf(leibniz_t, type, l: A > A > $o).
thf(leibniz_def, definition,
  l = ^[X, Y]: ![P]: P @ X <= P @ Y
).
"""

leibniz3 = """
thf(leibniz_t, type, l: A > A > $o).
thf(leibniz_def, definition,
  l = ^[X, Y]: ![P]: P @ X <=> P @ Y
).
"""

andrews = """
thf(andrews_t, type, a: A > A > $o).
thf(andrews_def, definition,
  a = ^[X, Y]: ![Q]: ((![Z]: Q @ Z @ Z) => Q @ X @ Y)
).
"""

extensional = """
thf(extensional_t, type, e: (A>B) > (A>B) > $o).
thf(extensional_def, definition,
  e = ^[X, Y]: ![Z]: X @ Z = Y @ Z
).
"""

Examples

Trivial:

~f"![X,Y]: X | Y => Y | X" |> prove

requires $\mathfrak{b}$:

~f"![X,Y]: X | Y = Y | X" |> prove

res = ~p"""
#{leibniz1}
thf(conj, conjecture,
  ![X,Y]: (l @ (X | Y) @ (Y | X))
).
""" |> prove

res = ~p"""
#{leibniz2}
thf(conj, conjecture,
  ![X,Y]: (l @ (X | Y) @ (Y | X))
).
""" |> prove

res = ~p"""
#{leibniz3}
thf(conj, conjecture,
  ![X,Y]: (l @ (X | Y) @ (Y | X))
).
""" |> prove

res = ~p"""
#{andrews}
thf(conj, conjecture,
  ![X,Y]: (a @ (X | Y) @ (Y | X))
).
""" |> prove

requires $\mathfrak{b}$ and $\xi$:

res = ~f"(^[X,Y]: X | Y) = (^[X,Y]: Y | X)" |> prove

res = ~p"""
#{leibniz1}
thf(conj, conjecture,
  l @ (^[X,Y]: X | Y) @ (^[X,Y]: Y | X)
).
""" |> prove

res = ~p"""
#{leibniz2}
thf(conj, conjecture,
  l @ (^[X,Y]: X | Y) @ (^[X,Y]: Y | X)
).
""" |> prove

res = ~p"""
#{leibniz3}
thf(conj, conjecture,
  l @ (^[X,Y]: X | Y) @ (^[X,Y]: Y | X)
).
""" |> prove

res = ~p"""
#{andrews}
thf(conj, conjecture,
  a @ (^[X,Y]: X | Y) @ (^[X,Y]: Y | X)
).
""" |> prove

res = ~p"""
#{extensional}
thf(conj, conjecture,
  e @ (^[X,Y]: X | Y) @ (^[X,Y]: Y | X)
).
""" |> prove

requires $\mathfrak{b}$ and $\mathfrak{f}$:

~f"(&) = ^[X,Y]: Y & X" |> prove

res = ~p"""
#{leibniz1}
thf(conj,conjecture,
  l @ (&) @ (^[X,Y]: Y & X)
).
""" |> prove

res = ~p"""
#{leibniz2}
thf(conj,conjecture,
  l @ (&) @ (^[X,Y]: Y & X)
).
""" |> prove

res = ~p"""
#{leibniz3}
thf(conj,conjecture,
  l @ (&) @ (^[X,Y]: Y & X)
).
""" |> prove

res = ~p"""
#{andrews}
thf(conj,conjecture,
  a @ (&) @ (^[X,Y]: Y & X)
).
""" |> prove

res = ~p"""
#{extensional}
thf(conj,conjecture,
  e @ (&) @ (^[X,Y]: Y & X)
).
""" |> prove

requires $\mathfrak{b}$:

res = ~f"p @ a & p @ b => p @ (a & b)" |> prove

res = with_context(~e[h:$o>$i], fn ->
  ~f"h @ (h @ $true = h @ $false) = h @ $false"
end) |> prove

render res

res = ~p"""
#{leibniz1}
thf(h_t, type, h: $o>$i).
thf(conj,conjecture,
  l @ (h @ (l @ (h @ $true) @ (h @ $false))) @ (h @ $false)
).
""" |> prove

res = ~p"""
#{leibniz2}
thf(h_t, type, h: $o>$i).
thf(conj,conjecture,
  l @ (h @ (l @ (h @ $true) @ (h @ $false))) @ (h @ $false)
).
""" |> prove

res = ~p"""
#{leibniz3}
thf(h_t, type, h: $o>$i).
thf(conj,conjecture,
  l @ (h @ (l @ (h @ $true) @ (h @ $false))) @ (h @ $false)
).
""" |> prove

res = ~p"""
#{andrews}
thf(h_t, type, h: $o>$i).
thf(conj,conjecture,
  a @ (h @ (a @ (h @ $true) @ (h @ $false))) @ (h @ $false)
).
""" |> prove

res = with_context(~e[h:$o>$i], fn ->
  ~f"(c @ (h @ $false)) & (h @ $true = h @ $false) => c @ (h @ $true)"
end) |> prove

res = with_context(~e[h:$o>$i], fn ->
  ~f"(c @ (h @ $false)) & (h @ $true = h @ X) => c @ (h @ $true)"
end) |> prove

# Generated by SystemOnTPTP Smart Cell
problem = "thf(p_type, type, h: $o>$i).\r\nthf(test, conjecture,\r\n    (h @ ((h @ $true) = (h @ $false))) = (h @ $false)\r\n)."
system_name = "Leo-III---1.7.20"
time_limit = 5

case AtpClient.SystemOnTptp.query_system(problem, system_name, time_limit_sec: time_limit, raw: true) do
  {:ok, result} ->
    IO.puts(result)
    result

  {:error, reason} ->
    raise "Error: #{inspect(reason)}"
end

(skipped) examples valid in all model classes…

Non-trivial direction of Boolean extensionality:

~f"![A,B]: ( (A <=> B) => A = B )" |> prove

~p"""
thf(h,type,
    h: ( $i > $o ) > $i ).

thf(cTHM573_pme,conjecture,
    ( ! [Xx: $i > $o,Xy: $i > $o] :
        ( ( ( h @ Xx )
          = ( h @ Xy ) )
       => ( Xx = Xy ) )
   => ? [Xg: $i > $i > $o] :
      ! [Y: $i > $o] :
      ? [X: $i] :
        ( ( Xg @ X )
        = Y ) ) ).
""" |> prove

# Generated by SystemOnTPTP Smart Cell
problem = "thf(conj,conjecture,\n    ~ ? [H: ( $i > $o ) > $i] :\n      ! [P: $i > $o,Q: $i > $o] :\n        ( ( ( H @ P )\n          = ( H @ Q ) )\n       => ( P = Q ) ) )."
system_name = "Vampire---5.0.1"
time_limit = 5

case AtpClient.SystemOnTptp.query_system(problem, system_name, time_limit_sec: time_limit, raw: true) do
  {:ok, result} ->
    IO.puts(result)
    result

  {:error, reason} ->
    raise "Error: #{inspect(reason)}"
end

~p"""
thf(conj,conjecture,
    ~ ? [H: ( $i > $o ) > $i] :
      ! [P: $i > $o,Q: $i > $o] :
        ( ( ( H @ P )
          = ( H @ Q ) )
       => ( P = Q ) ) ).
""" |> prove