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

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

Examples

Trivial:

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

requires $\mathfrak{b}$:

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

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

render res

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

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

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

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

render res

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

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

requires $\mathfrak{b}$:

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

render res

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

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

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(test, conjecture, $true => $true)."
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

render res

# 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"
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