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

``````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)``````