First-Order Logic System

A First-Order Logic System is a Predicate Logic System that allows the representation of logic terms, predicate symbols, function symbols, constant symbols, and of Quantification over Variables.

• AKA: Lower Predicate Calculus, LPC, First-Order Predicate Calculus, First-Order Theory, F Logic, First-Order Predicate Logic, FOPL.
• Context:
  • It must have a set of First-Order Sentence/First-Order Logic Formulas (a First-Order Logic Language).
  • It must have a set of First-Order Logic Operations.
  • Logic Terms: name Objects or sets of objects
    • Constants: Represent a specific object.
    • Variables: Represent an unnamed object; or all objects of a kind, depending on the quantifier.
    • Functions: Map a Tuple of [math]\displaystyle{ n }[/math] terms to another term.
  • Predicate: Describe the relations that hold among a fixed number of objects in a given domain.
  • Connectives: Allow predicates to be combined into more complex representations. (E.g. AND, NOT)
  • Quantifiers: Allow statements against classes of objects without having to enumerate them by name. (e.g. existential and universal.)
    • Universal Quantifier: A Statement is true for all Values of the Variable.
    • Existential Quantifier: A Statement is true for at least one Value of the Variable.
  • It can be use as an Ontology Language to represent a Domain.
  • Is Turing Complete (Computationally Tractable).
  • It can be associated with a First-Order Logic Model.
  • …
• Counter-Example(s):
  • a Default Logic System.
  • a Propositional Logic System.
  • a Finite Automata Language.
• See: Deductive Reasoning; Horn Clause; Inductive Logic Programming; Second-Order Logic; Relational Calculus; Lambda Calculus; Markov Logic Network; Descriptive Logic; Abduction; Entailment; Higher-Order Logic; Hypothesis Language; Inductive Logic Programming; Learning from Structured Data; Logic Program; Propositionalization; Relational Data Mining, Predicate Logic, Propositional Logic, Quantifier#Logic, Higher-Order Logic, Deductive System, Completeness (Logic).

---

---

References

2018

• (Hughes & Schagrin, 2018) ⇒ G.E. Hughes, and Morton L. Schagrin (November 02, 2018). Formal logic: https://www.britannica.com/topic/formal-logic/The-predicate-calculus#ref65843 Retrieved: 2019-06-09. In: Encyclopaedia Britannica.
  • QUOTE: A predicate calculus in which the only variables that occur in quantifiers are individual variables is known as a lower (or first-order) predicate calculus.

2015

• (Russell, 2015) ⇒ Stuart Russell. (2015). “Unifying Logic and Probability.” In: Communications of the ACM Journal, 58(7). doi:10.1145/2699411
  • QUOTE: For example, the rules of chess occupy 100 pages in first-order logic, 105 pages in propositional logic, and 1038 pages in the language of finite automata. The power comes from separating predicates from their arguments and quantifying over those arguments: so one can write rules about On (p, c, x, y, t) (piece p of color c is on square x, y at move t) without filling in each specific value for c, p, x, y, and t.

2014

• (Wikipedia, 2014) ⇒ http://en.wikipedia.org/wiki/first-order_logic Retrieved:2014-8-6.
  • First-order logic is a formal system used in mathematics, philosophy, linguistics, and computer science. It is also known as first-order predicate calculus, the lower predicate calculus, quantification theory, and predicate logic. First-order logic is distinguished from propositional logic by its use of quantified variables.

    A theory about some topic is usually first-order logic together with a specified domain of discourse over which the quantified variables range, finitely many functions which map from that domain into it, finitely many predicates defined on that domain, and a recursive set of axioms which are believed to hold for those things. Sometimes "theory" is understood in a more formal sense, which is just a set of sentences in first-order logic.

    The adjective "first-order" distinguishes first-order logic from higher-order logic in which there are predicates having predicates or functions as arguments, or in which one or both of predicate quantifiers or function quantifiers are permitted. In first-order theories, predicates are often associated with sets. In interpreted higher-order theories, predicates may be interpreted as sets of sets.

    There are many deductive systems for first-order logic that are sound (all provable statements are true in all models) and complete (all statements which are true in all models are provable). Although the logical consequence relation is only semidecidable, much progress has been made in automated theorem proving in first-order logic. First-order logic also satisfies several metalogical theorems that make it amenable to analysis in proof theory, such as the Löwenheim–Skolem theorem and the compactness theorem.

    First-order logic is the standard for the formalization of mathematics into axioms and is studied in the foundations of mathematics. Mathematical theories, such as number theory and set theory, have been formalized into first-order axiom schemata such as Peano arithmetic and Zermelo–Fraenkel set theory (ZF) respectively.

    No first-order theory, however, has the strength to describe fully and categorically structures with an infinite domain, such as the natural numbers or the real line. Categorical axiom systems for these structures can be obtained in stronger logics such as second-order logic.

    For a history of first-order logic and how it came to dominate formal logic, see José Ferreirós (2001).

2013

• (Genesereth & Kao, 2013) ⇒ Michael Genesereth, and Eric Kao. (2013). “Introduction to Logic." Morgan & Claypool Publishers. doi:10.2200/S00432ED1V01Y201207CSL005

2011

• (Flach, 2011a) ⇒ Peter A. Flach. (2011). “First-Order Logic.” In: (Sammut & Webb, 2011) p.410

• http://www.chemistrydaily.com/chemistry/First-order_logic
  • A first-order theory is a theory that can be axiomatised as an extension of first-order logic by adding a recursive set of first-order sentences as axioms.
• http://encyclopedia.kids.net.au/page/fi/First-order_predicate_calculus
  • Permits the formulation of quantified statements such as "there exists an x such that..." () or "for any x, it is the case that...", where x is a member of the domain of discourse.
• CYC Glossary http://www.cyc.com/cycdoc/ref/glossary.html
  • first-order predicate calculus (FOPC): A formal language incorporating predicate symbols, function symbols, constant symbols, variables, logical connectives and quantifiers, which can be used to express facts about a world. Unlike propositional logic, FOPC can express general statements or statements about existence, by using quantified variables. “First-order" means that statements which quantify over predicate and function symbols are not allowed.

---