LARA

First-Order Logic Constructs

The following constructs define formulas:

/** Literal true. */
case object True extends Formula

/** Literal false. */
case object False extends Formula

/** Negation. */
case class Not(inner: Formula) extends Formula

/** Conjunction. */
case class And(lhs: Formula, rhs: Formula) extends Formula

/** Disjunction. */
case class Or(lhs: Formula, rhs: Formula) extends Formula

/** Implication. */
case class Implies(lhs: Formula, rhs: Formula) extends Formula

/** Equivalence. */
case class Iff(lhs: Formula, rhs: Formula) extends Formula

/** Universal quantification. */
case class Forall(id: Identifier, inner: Formula) extends Formula

/** Existential quantification. */
case class Exists(id: Identifier, inner: Formula) extends Formula

/** Equality between expressions. */
case class Equals(lhs: Expr, rhs: Expr) extends Formula

/** Predicate application. */
case class PredApp(predicate: Predicate, args: Seq[Expr]) extends Formula

Where the expressions are defined as follows.

/** Constant expression. */
case class Con(constant: Constant) extends Expr

/** Variable. */
case class Var(id: Identifier) extends Expr

/** Function application. */
case class FunApp(function: Function, args: Seq[Expr]) extends Expr

Finally, all of the following types are simply defined as strings.

/** Type of primitive expressions. */
type Constant = String

/** Type for identifiers. */
type Identifier = String

/** Type for functions. */
type Function = String

/** Type for predicates. */
type Predicate = String

Quasiquoter

For your convenience, a quasiquoter is provided so that you can write formulas more easily. Below are a few examples.

import fol._
fol"P"
// res0: PredApp = PredApp("P", List())
fol"P(x, f(y))"
// res1: PredApp = PredApp("P", List(Var("x"), FunApp("f", List(Var("y")))))
fol"f(x) = x"
// res2: Equals = Equals(FunApp("f", List(Var("x"))), Var("x"))
fol"x != 'a"
// res3: Not = Not(Equals(Var("x"), Con("a")))
fol"P \/ ~Q"
// res4: Or = Or(PredApp("P", List()), Not(PredApp("Q", List())))
fol"P /\ Q /\ R"
// res5: And = And(
//   PredApp("P", List()),
//   And(PredApp("Q", List()), PredApp("R", List()))
// )
fol"P /\ Q \/ R"
// res6: Or = Or(
//   And(PredApp("P", List()), PredApp("Q", List())),
//   PredApp("R", List())
// )
fol"P /\ Q => P \/ Q"
// res7: Implies = Implies(
//   And(PredApp("P", List()), PredApp("Q", List())),
//   Or(PredApp("P", List()), PredApp("Q", List()))
// )
fol"forall x. exists y. x = y"
// res8: Forall = Forall("x", Exists("y", Equals(Var("x"), Var("y"))))
fol"forall x y. x = y <=> y = x"
// res9: Forall = Forall(
//   "x",
//   Forall("y", Iff(Equals(Var("x"), Var("y")), Equals(Var("y"), Var("x"))))
// )

All binary operators (i.e. \/, /\, =>, <=>) are right-associative.

fol"P => Q => R"
// res10: Implies = Implies(
//   PredApp("P", List()),
//   Implies(PredApp("Q", List()), PredApp("R", List()))
// )
fol"P <=> Q <=> R"
// res11: Iff = Iff(
//   PredApp("P", List()),
//   Iff(PredApp("Q", List()), PredApp("R", List()))
// )

Operator precedence is as you would expect: Conjunction binds stronger than disjunction, which binds stronger than implication, which binds stronger than equivalence.

fol"P /\ Q \/ R => S <=> T"
// res12: Iff = Iff(
//   Implies(
//     Or(And(PredApp("P", List()), PredApp("Q", List())), PredApp("R", List())),
//     PredApp("S", List())
//   ),
//   PredApp("T", List())
// )
fol"P <=> Q => R \/ S /\ T"
// res13: Iff = Iff(
//   PredApp("P", List()),
//   Implies(
//     PredApp("Q", List()),
//     Or(PredApp("R", List()), And(PredApp("S", List()), PredApp("T", List())))
//   )
// )

Parentheses can be used to force other interpretations.

fol"((P <=> Q) => (R \/ S)) /\ T"
// res14: And = And(
//   Implies(
//     Iff(PredApp("P", List()), PredApp("Q", List())),
//     Or(PredApp("R", List()), PredApp("S", List()))
//   ),
//   PredApp("T", List())
// )

Holes

The quasiquoter supports holes.

val x = "x"
// x: String = "x"
val f = fol"$x = $x"
// f: Equals = Equals(Var("x"), Var("x"))
fol"forall $x. $f"
// res15: Forall = Forall("x", Equals(Var("x"), Var("x")))

When the hole is to be filled with something more complex than a simple variable, the following syntax can be used:

def foo(f: Formula): Formula = Iff(f, f)
fol"forall x. ${foo(True)}"
// res16: Forall = Forall("x", Iff(True, True))

In the case of predicates and functions, it is possible to fill a hole with a sequence of arguments, using the syntax ..$elems.

val elems = Seq.tabulate(10)(i => Var("x" + i))
// elems: Seq[Var] = List(
//   Var("x0"),
//   Var("x1"),
//   Var("x2"),
//   Var("x3"),
//   Var("x4"),
//   Var("x5"),
//   Var("x6"),
//   Var("x7"),
//   Var("x8"),
//   Var("x9")
// )
fol"p(..$elems)"
// res17: PredApp = PredApp(
//   "p",
//   List(
//     Var("x0"),
//     Var("x1"),
//     Var("x2"),
//     Var("x3"),
//     Var("x4"),
//     Var("x5"),
//     Var("x6"),
//     Var("x7"),
//     Var("x8"),
//     Var("x9")
//   )
// )

Pattern-Matching

The quasiquoter can also be used as a pattern. In this case, the holes are filled with the values matched.

Iff(PredApp("P", Seq(Var("x"))), Equals(Var("x"), Var("y"))) match {
  case fol"$p /\ $q" => println("Wrong case.")
  case fol"$p(..$xs) <=> $q" => {
    println("Matched !")
    println("p = " + p)
    println("xs = " + xs)
    println("q = " + q)
  }
  case _ => println("Not matched.")
}
// Matched !
// p = P
// xs = List(Var(x))
// q = Equals(Var(x),Var(y))

Pretty Printing

By default, the formulas and expressions are displayed in terms of the various constructors. Formulas offer a method .pretty which produces a pretty printed version.

println(Iff(PredApp("P", Seq(Var("x"))), Equals(Var("x"), Var("y"))).pretty)
// P(x) ⇔ x = y

LCF

The library for LCF that we use is located in the package lcf. Since we will also need to manipulate formulas, we import the package fol.

import fol._
import lcf._

In the LCF approach, proven formulas are wrapped in a separate class called Theorem.

val ex: Theorem = refl(expr"x")
// ex: Theorem = Equals(Var(x),Var(x))
println(ex.pretty)
// ⊢ x = x

The constructor of Theorem is private, and thus new theorems can only be obtained from a provided set of axioms and rules, which are listed below.

The formula proven by a theorem can be obtained through the .formula method.

ex.formula
// res1: Formula = Equals(Var("x"), Var("x"))

Rules

There are only two primitive rules that can derive a theorem from other theorems: modus ponens and generalisation.

/** Modus ponens rule.
  *
  * Given a theorem of `P => Q`, and a theorem of `P`, produces a theorem of `Q`.
  */
def modusPonens(pq: Theorem, p: Theorem): Theorem = pq.formula match {
  case Implies(pf, qf) if p.formula == pf => Theorem(qf)  // Note the use of the Theorem constructor.
  case _ => throw new IllegalArgumentException("Illegal application of modusPonens.")
}

/** Generalisation.
  *
  * Given a theorem of `P` and an identifier `x`, produces a theorem of `forall x. P`.
  */
def generalize(p: Theorem, x: Identifier): Theorem = {
  Theorem(Forall(x, p.formula))  // Note the use of the Theorem constructor.
}

Axioms

In addition of the two inference rules, the system comes with a basic set of axiom schemas:

Addition of premise

println(addImplies(fol"P", fol"Q").pretty)
// ⊢ P ⇒ Q ⇒ P

Distributivity of implication

println(impliesDistr(fol"P", fol"Q", fol"R").pretty)
// ⊢ (P ⇒ Q ⇒ R) ⇒ (P ⇒ Q) ⇒ P ⇒ R

Double negation

println(doubleNegation(fol"P").pretty)
// ⊢ ((P ⇒ ⊥) ⇒ ⊥) ⇒ P

Application under forall

println(forallImplies("x", fol"P", fol"Q").pretty)
// ⊢ (∀x. P ⇒ Q) ⇒ (∀x. P) ⇒ (∀x. Q)

Forall introduction

println(forallIntro("x", fol"P").pretty)
// ⊢ P ⇒ (∀x. P)
try {
  println(forallIntro("x", fol"P(x)").pretty)
}
catch {
  case e: Exception => println(e)
}
// java.lang.IllegalArgumentException: Illegal application of forallIntro: identifier is free in the formula.

Existence of a witness

println(existsEquals("x", expr"f(y)").pretty)
// ⊢ ∃x. x = f(y)
try {
  println(existsEquals("x", expr"f(x)").pretty)
}
catch {
  case e: Exception => println(e)
}
// java.lang.IllegalArgumentException: Illegal application of existsEquals: identifier is free in the expression.

Reflexivity of equality

println(refl(expr"f(x)").pretty)
// ⊢ f(x) = f(x)

Congruence

println(funCongruence("f", Seq(expr"x1", expr"x2"), Seq(expr"y1", expr"y2")).pretty)
// ⊢ x1 = y1 ⇒ x2 = y2 ⇒ f(x1, x2) = f(y1, y2)
println(predCongruence("P", Seq(expr"x1", expr"x2"), Seq(expr"y1", expr"y2")).pretty)
// ⊢ x1 = y1 ⇒ x2 = y2 ⇒ P(x1, x2) ⇒ P(y1, y2)
println(equCongruence(expr"x1", expr"x2", expr"y1", expr"y2").pretty)
// ⊢ x1 = y1 ⇒ x2 = y2 ⇒ x1 = x2 ⇒ y1 = y2

Conversion between constructs

println(impliesToIff(fol"P", fol"Q").pretty)
// ⊢ (P ⇒ Q) ⇒ (Q ⇒ P) ⇒ (P ⇔ Q)
println(iffToImplies1(fol"P", fol"Q").pretty)
// ⊢ (P ⇔ Q) ⇒ P ⇒ Q
println(iffToImplies2(fol"P", fol"Q").pretty)
// ⊢ (P ⇔ Q) ⇒ Q ⇒ P
println(trueIff.pretty)
// ⊢ ⊤ ⇔ ⊥ ⇒ ⊥
println(notIff(fol"P").pretty)
// ⊢ ¬P ⇔ P ⇒ ⊥
println(andIff(fol"P", fol"Q").pretty)
// ⊢ P ∧ Q ⇔ (P ⇒ Q ⇒ ⊥) ⇒ ⊥
println(orIff(fol"P", fol"Q").pretty)
// ⊢ P ∨ Q ⇔ ¬(¬P ∧ ¬Q)
println(existsIff("x", fol"P").pretty)
// ⊢ (∃x. P) ⇔ ¬(∀x. ¬P)