Communication
Faster access than browser!

# First-order logic

First-order logic—also known as first-order predicate calculus and predicate logic—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. [1]

## Abelian group

In abstract algebra, an abelian group, also called a commutative group, is a group in which the result of applying the group operation to two group elements does not depend on the order in which they are written.

## Abstract algebra

In algebra, which is a broad division of mathematics, abstract algebra (occasionally called modern algebra) is the study of algebraic structures.

## ACL2

ACL2 (A Computational Logic for Applicative Common Lisp) is a software system consisting of a programming language, an extensible theory in a first-order logic, and a mechanical theorem prover.

## Alan Turing

Alan Mathison Turing (23 June 1912 – 7 June 1954) was an English computer scientist, mathematician, logician, cryptanalyst, philosopher, and theoretical biologist.

## Alfred Tarski

Alfred Tarski (January 14, 1901 &ndash; October 26, 1983), born Alfred Teitelbaum,School of Mathematics and Statistics, University of St Andrews,, School of Mathematics and Statistics, University of St Andrews.

## Algebra

Algebra (from Arabic "al-jabr", literally meaning "reunion of broken parts") is one of the broad parts of mathematics, together with number theory, geometry and analysis.

## Alonzo Church

Alonzo Church (June 14, 1903 – August 11, 1995) was an American mathematician and logician who made major contributions to mathematical logic and the foundations of theoretical computer science.

## Amsterdam

Amsterdam is the capital and most populous municipality of the Netherlands.

## Arithmetic

Arithmetic (from the Greek ἀριθμός arithmos, "number") is a branch of mathematics that consists of the study of numbers, especially the properties of the traditional operations on them—addition, subtraction, multiplication and division.

## Arity

In logic, mathematics, and computer science, the arity of a function or operation is the number of arguments or operands that the function takes.

## Atomic formula

In mathematical logic, an atomic formula (also known simply as an atom) is a formula with no deeper propositional structure, that is, a formula that contains no logical connectives or equivalently a formula that has no strict subformulas.

## Atomic sentence

In logic, an atomic sentence is a type of declarative sentence which is either true or false (may also be referred to as a proposition, statement or truthbearer) and which cannot be broken down into other simpler sentences.

## Automated proof checking

Automated proof checking is the process of using software for checking proofs for correctness.

## Automated theorem proving

Automated theorem proving (also known as ATP or automated deduction) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs.

## Axiom

An axiom or postulate is a statement that is taken to be true, to serve as a premise or starting point for further reasoning and arguments.

## Axiom of choice

In mathematics, the axiom of choice, or AC, is an axiom of set theory equivalent to the statement that the Cartesian product of a collection of non-empty sets is non-empty.

## Axiom of empty set

In axiomatic set theory, the axiom of empty set is an axiom of Kripke–Platek set theory and the variant of general set theory that Burgess (2005) calls "ST," and a demonstrable truth in Zermelo set theory and Zermelo–Fraenkel set theory, with or without the axiom of choice.

## Axiom of extensionality

In axiomatic set theory and the branches of logic, mathematics, and computer science that use it, the axiom of extensionality, or axiom of extension, is one of the axioms of Zermelo–Fraenkel set theory.

## Axiom schema

In mathematical logic, an axiom schema (plural: axiom schemata or axiom schemas) generalizes the notion of axiom.

## Axiomatic system

In mathematics, an axiomatic system is any set of axioms from which some or all axioms can be used in conjunction to logically derive theorems.

## Ben Goertzel

Ben Goertzel (born December 8, 1966) is the founder and CEO of SingularityNET, a blockchain-based AI marketplace.

## Bernays–Schönfinkel class

The Bernays–Schönfinkel class (also known as Bernays–Schönfinkel-Ramsey class) of formulas, named after Paul Bernays and Moses Schönfinkel (and Frank P. Ramsey), is a fragment of first-order logic formulas where satisfiability is decidable.

## Binary relation

In mathematics, a binary relation on a set A is a set of ordered pairs of elements of A. In other words, it is a subset of the Cartesian product A2.

## Boolean-valued function

A Boolean-valued function (sometimes called a predicate or a proposition) is a function of the type f: X → B, where X is an arbitrary set and where B is a Boolean domain, i.e. a generic two-element set, (for example B.

## Bounded quantifier

In the study of formal theories in mathematical logic, bounded quantifiers are often included in a formal language in addition to the standard quantifiers "∀" and "∃".

## Branching quantifier

In logic a branching quantifier, also called a Henkin quantifier, finite partially ordered quantifier or even nonlinear quantifier, is a partial ordering of quantifiers for Q ∈.

## Cardinal number

In mathematics, cardinal numbers, or cardinals for short, are a generalization of the natural numbers used to measure the cardinality (size) of sets.

## Cardinality

In mathematics, the cardinality of a set is a measure of the "number of elements of the set".

## Central processing unit

A central processing unit (CPU) is the electronic circuitry within a computer that carries out the instructions of a computer program by performing the basic arithmetic, logical, control and input/output (I/O) operations specified by the instructions.

## Charles Sanders Peirce

Charles Sanders Peirce ("purse"; 10 September 1839 – 19 April 1914) was an American philosopher, logician, mathematician, and scientist who is sometimes known as "the father of pragmatism".

## Compactness theorem

In mathematical logic, the compactness theorem states that a set of first-order sentences has a model if and only if every finite subset of it has a model.

## Complete theory

In mathematical logic, a theory is complete if, for every formula in the theory's language, that formula or its negation is demonstrable.

## Completeness (logic)

In mathematical logic and metalogic, a formal system is called complete with respect to a particular property if every formula having the property can be derived using that system, i.e. is one of its theorems; otherwise the system is said to be incomplete.

## Computational complexity theory

Computational complexity theory is a branch of the theory of computation in theoretical computer science that focuses on classifying computational problems according to their inherent difficulty, and relating those classes to each other.

## Computer science

Computer science deals with the theoretical foundations of information and computation, together with practical techniques for the implementation and application of these foundations.

## Congruence relation

In abstract algebra, a congruence relation (or simply congruence) is an equivalence relation on an algebraic structure (such as a group, ring, or vector space) that is compatible with the structure.

## Connected component (graph theory)

In graph theory, a connected component (or just component) of an undirected graph is a subgraph in which any two vertices are connected to each other by paths, and which is connected to no additional vertices in the supergraph.

## Consistency

In classical deductive logic, a consistent theory is one that does not contain a contradiction.

## Context-free grammar

In formal language theory, a context-free grammar (CFG) is a certain type of formal grammar: a set of production rules that describe all possible strings in a given formal language.

## Countable set

In mathematics, a countable set is a set with the same cardinality (number of elements) as some subset of the set of natural numbers.

## Cylindric algebra

The notion of cylindric algebra, invented by Alfred Tarski, arises naturally in the algebraization of equational first-order logic.

## Data type

In computer science and computer programming, a data type or simply type is a classification of data which tells the compiler or interpreter how the programmer intends to use the data.

## David Hilbert

David Hilbert (23 January 1862 – 14 February 1943) was a German mathematician.

## Decidability (logic)

In logic, the term decidable refers to the decision problem, the question of the existence of an effective method for determining membership in a set of formulas, or, more precisely, an algorithm that can and will return a boolean true or false value that is correct (instead of looping indefinitely, crashing, returning "don't know" or returning a wrong answer).

## Decision problem

In computability theory and computational complexity theory, a decision problem is a problem that can be posed as a yes-no question of the input values.

## Description logic

Description logics (DL) are a family of formal knowledge representation languages.

## Directed graph

In mathematics, and more specifically in graph theory, a directed graph (or digraph) is a graph that is a set of vertices connected by edges, where the edges have a direction associated with them.

## Domain of discourse

In the formal sciences, the domain of discourse, also called the universe of discourse, universal set, or simply universe, is the set of entities over which certain variables of interest in some formal treatment may range.

## Dover Publications

Dover Publications, also known as Dover Books, is an American book publisher founded in 1941 by Hayward Cirker and his wife, Blanche.

## Elementary class

In model theory, a branch of mathematical logic, an elementary class (or axiomatizable class) is a class consisting of all structures satisfying a fixed first-order theory.

## Empty set

In mathematics, and more specifically set theory, the empty set or null set is the unique set having no elements; its size or cardinality (count of elements in a set) is zero.

## Entscheidungsproblem

In mathematics and computer science, the Entscheidungsproblem (German for "decision problem") is a challenge posed by David Hilbert in 1928.

## Equiconsistency

In mathematical logic, two theories are equiconsistent if the consistency of one theory implies the consistency of the other theory, and vice versa.

## Equivalence relation

In mathematics, an equivalence relation is a binary relation that is reflexive, symmetric and transitive.

## Exclusive or

Exclusive or or exclusive disjunction is a logical operation that outputs true only when inputs differ (one is true, the other is false).

## Existential quantification

In predicate logic, an existential quantification is a type of quantifier, a logical constant which is interpreted as "there exists", "there is at least one", or "for some".

## Extension by definitions

In mathematical logic, more specifically in the proof theory of first-order theories, extensions by definitions formalize the introduction of new symbols by means of a definition.

## Formal grammar

In formal language theory, a grammar (when the context is not given, often called a formal grammar for clarity) is a set of production rules for strings in a formal language.

## Formal language

In mathematics, computer science, and linguistics, a formal language is a set of strings of symbols together with a set of rules that are specific to it.

## Formal specification

In computer science, formal specifications are mathematically based techniques whose purpose are to help with the implementation of systems and software.

## Formal system

A formal system is the name of a logic system usually defined in the mathematical way.

## Formal verification

In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics.

## Formation rule

In mathematical logic, formation rules are rules for describing which strings of symbols formed from the alphabet of a formal language are syntactically valid within the language.

## Foundations of mathematics

Foundations of mathematics is the study of the philosophical and logical and/or algorithmic basis of mathematics, or, in a broader sense, the mathematical investigation of what underlies the philosophical theories concerning the nature of mathematics.

## Free logic

A free logic is a logic with fewer existential presuppositions than classical logic.

## Gödel's completeness theorem

Gödel's completeness theorem is a fundamental theorem in mathematical logic that establishes a correspondence between semantic truth and syntactic provability in first-order logic.

## Gödel's incompleteness theorems

Gödel's incompleteness theorems are two theorems of mathematical logic that demonstrate the inherent limitations of every formal axiomatic system containing basic arithmetic.

## George Boolos

George Stephen Boolos (September 4, 1940 – May 27, 1996) was an American philosopher and a mathematical logician who taught at the Massachusetts Institute of Technology.

## George Edward Hughes

George Edward Hughes (8 June 1918 – 4 March 1994) was an Irish-born New Zealand philosopher and logician whose principal scholarly works were concerned with modal logic and medieval philosophy.

## Gottlob Frege

Friedrich Ludwig Gottlob Frege (8 November 1848 – 26 July 1925) was a German philosopher, logician, and mathematician.

## Graph (discrete mathematics)

In mathematics, and more specifically in graph theory, a graph is a structure amounting to a set of objects in which some pairs of the objects are in some sense "related".

## Group (mathematics)

In mathematics, a group is an algebraic structure consisting of a set of elements equipped with an operation that combines any two elements to form a third element and that satisfies four conditions called the group axioms, namely closure, associativity, identity and invertibility.

## Guarded logic

Guarded logic is a choice set of dynamic logic involved in choices, where outcomes are limited.

## Halting problem

In computability theory, the halting problem is the problem of determining, from a description of an arbitrary computer program and an input, whether the program will finish running (i.e., halt) or continue to run forever.

## Heinz-Dieter Ebbinghaus

Heinz-Dieter Ebbinghaus (born 22 February 1939 in Hemer, Province of Westphalia) is a German mathematician and logician.

## Herbrandization

The Herbrandization of a logical formula (named after Jacques Herbrand) is a construction that is dual to the Skolemization of a formula.

## Heuristic (computer science)

In computer science, artificial intelligence, and mathematical optimization, a heuristic (from Greek εὑρίσκω "I find, discover") is a technique designed for solving a problem more quickly when classic methods are too slow, or for finding an approximate solution when classic methods fail to find any exact solution.

## Higher-order logic

In mathematics and logic, a higher-order logic is a form of predicate logic that is distinguished from first-order logic by additional quantifiers and, sometimes, stronger semantics.

## Hilbert system

In logic, especially mathematical logic, a Hilbert system, sometimes called Hilbert calculus, Hilbert-style deductive system or Hilbert&ndash;Ackermann system, is a type of system of formal deduction attributed to Gottlob FregeMáté & Ruzsa 1997:129 and David Hilbert.

## Interpretation (logic)

An interpretation is an assignment of meaning to the symbols of a formal language.

## Intuitionistic logic

Intuitionistic logic, sometimes more generally called constructive logic, refers to systems of symbolic logic that differ from the systems used for classical logic by more closely mirroring the notion of constructive proof.

## Isabelle (proof assistant)

The Isabelle theorem prover is an interactive theorem prover, a Higher Order Logic (HOL) theorem prover.

## Józef Maria Bocheński

Józef Maria Bocheński (Czuszów, Congress Poland, Russian Empire, 30 August 1902 – 8 February 1995, Fribourg, Switzerland) was a Polish Dominican, logician and philosopher.

## John Etchemendy

John W. Etchemendy (born 1952 in Reno, Nevada) was Stanford University's twelfth Provost.

## Jon Barwise

Kenneth Jon Barwise (June 29, 1942 – March 5, 2000) was an American mathematician, philosopher and logician who proposed some fundamental revisions to the way that logic is understood and used.

## Kurt Gödel

Kurt Friedrich Gödel (April 28, 1906 – January 14, 1978) was an Austrian, and later American, logician, mathematician, and philosopher.

L.

## Lattice (order)

A lattice is an abstract structure studied in the mathematical subdisciplines of order theory and abstract algebra.

## Löwenheim number

In mathematical logic the Löwenheim number of an abstract logic is the smallest cardinal number for which a weak downward Löwenheim–Skolem theorem holds.

## Löwenheim–Skolem theorem

In mathematical logic, the Löwenheim–Skolem theorem, named for Leopold Löwenheim and Thoralf Skolem, states that if a countable first-order theory has an infinite model, then for every infinite cardinal number κ it has a model of size κ. The result implies that first-order theories are unable to control the cardinality of their infinite models, and that no first-order theory with an infinite model can have a unique model up to isomorphism.

## Lindenbaum–Tarski algebra

In mathematical logic, the Lindenbaum–Tarski algebra (or Lindenbaum algebra) of a logical theory T consists of the equivalence classes of sentences of the theory (i.e., the quotient, under the equivalence relation ~ defined such that p ~ q exactly when p and q are provably equivalent in T).

## Lindström's theorem

In mathematical logic, Lindström's theorem (named after Swedish logician Per Lindström, who published it in 1969) states that first-order logic is the strongest logic (satisfying certain conditions, e.g. closure under classical negation) having both the (countable) compactness property and the (downward) Löwenheim–Skolem property.

## Linguistics

Linguistics is the scientific study of language, and involves an analysis of language form, language meaning, and language in context.

## List of first-order theories

In mathematical logic, a first-order theory is given by a set of axioms in some language.

## List of logic symbols

In logic, a set of symbols is commonly used to express logical representation.

## Logic of graphs

In the mathematical fields of graph theory and finite model theory, the logic of graphs deals with formal specifications of graph properties using logical formulas.

## Logical biconditional

In logic and mathematics, the logical biconditional (sometimes known as the material biconditional) is the logical connective of two statements asserting "P if and only if Q", where P is an antecedent and Q is a consequent.

## Logical conjunction

In logic, mathematics and linguistics, And (∧) is the truth-functional operator of logical conjunction; the and of a set of operands is true if and only if all of its operands are true.

## Logical connective

In logic, a logical connective (also called a logical operator, sentential connective, or sentential operator) is a symbol or word used to connect two or more sentences (of either a formal or a natural language) in a grammatically valid way, such that the value of the compound sentence produced depends only on that of the original sentences and on the meaning of the connective.

## Logical consequence

Logical consequence (also entailment) is a fundamental concept in logic, which describes the relationship between statements that hold true when one statement logically follows from one or more statements.

## Logical disjunction

In logic and mathematics, or is the truth-functional operator of (inclusive) disjunction, also known as alternation; the or of a set of operands is true if and only if one or more of its operands is true.

## Logical equality

Logical equality is a logical operator that corresponds to equality in Boolean algebra and to the logical biconditional in propositional calculus.

## Logical NOR

In boolean logic, logical nor or joint denial is a truth-functional operator which produces a result that is the negation of logical or.

## London

London is the capital and most populous city of England and the United Kingdom.

## Material conditional

The material conditional (also known as material implication, material consequence, or simply implication, implies, or conditional) is a logical connective (or a binary operator) that is often symbolized by a forward arrow "→".

## Mathematical proof

In mathematics, a proof is an inferential argument for a mathematical statement.

## Mathematics

Mathematics (from Greek μάθημα máthēma, "knowledge, study, learning") is the study of such topics as quantity, structure, space, and change.

## Max Cresswell

Maxwell John Cresswell (born 19 November 1939, Wellington) is a New Zealand philosopher and logician, known for his work in modal logic.

## Metalogic

Metalogic is the study of the metatheory of logic.

## Metamath

Metamath is a language for developing strictly formalized mathematical definitions and proofs accompanied by a proof checker for this language and a growing database of thousands of proved theorems covering conventional results in logic, set theory, number theory, group theory, algebra, analysis, and topology, as well as topics in Hilbert spaces and quantum logic.

## Method of analytic tableaux

In proof theory, the semantic tableau (plural: tableaux, also called 'truth tree') is a decision procedure for sentential and related logics, and a proof procedure for formulae of first-order logic.

## Mizar system

The Mizar system consists of a formal language for writing mathematical definitions and proofs, a proof assistant, which is able to mechanically check proofs written in this language, and a library of formalized mathematics, which can be used in the proof of new theorems.

## Modal logic

Modal logic is a type of formal logic primarily developed in the 1960s that extends classical propositional and predicate logic to include operators expressing modality.

## Model theory

In mathematics, model theory is the study of classes of mathematical structures (e.g. groups, fields, graphs, universes of set theory) from the perspective of mathematical logic.

## Modus ponens

In propositional logic, modus ponens (MP; also modus ponendo ponens (Latin for "mode that affirms by affirming") or implication elimination) is a rule of inference.

## Monadic predicate calculus

In logic, the monadic predicate calculus (also called monadic first-order logic) is the fragment of first-order logic in which all relation symbols in the signature are monadic (that is, they take only one argument), and there are no function symbols.

## Morley's categoricity theorem

In model theory, a branch of mathematical logic, a theory is κ-categorical (or categorical in κ) if it has exactly one model of cardinality κ up to isomorphism.

## Natural deduction

In logic and proof theory, natural deduction is a kind of proof calculus in which logical reasoning is expressed by inference rules closely related to the "natural" way of reasoning.

## Natural number

In mathematics, the natural numbers are those used for counting (as in "there are six coins on the table") and ordering (as in "this is the third largest city in the country").

## Negation

In logic, negation, also called the logical complement, is an operation that takes a proposition P to another proposition "not P", written \neg P (¬P), which is interpreted intuitively as being true when P is false, and false when P is true.

## New York City

The City of New York, often called New York City (NYC) or simply New York, is the most populous city in the United States.

## Non-logical symbol

In logic, the formal languages used to create expressions consist of symbols, which can be broadly divided into constants and variables.

## Non-standard model

In model theory, a discipline within mathematical logic, a non-standard model is a model of a theory that is not isomorphic to the intended model (or standard model).

## Nonfirstorderizability

In formal logic, nonfirstorderizability is the inability of an expression to be adequately captured in particular theories in first-order logic.

## Number theory

Number theory, or in older usage arithmetic, is a branch of pure mathematics devoted primarily to the study of the integers.

## Order of operations

In mathematics and computer programming, the order of operations (or operator precedence) is a collection of rules that reflect conventions about which procedures to perform first in order to evaluate a given mathematical expression.

## Ordered field

In mathematics, an ordered field is a field together with a total ordering of its elements that is compatible with the field operations.

## Ordered pair

In mathematics, an ordered pair (a, b) is a pair of objects.

## Pairing function

In mathematics, a pairing function is a process to uniquely encode two natural numbers into a single natural number.

## Paris

Paris is the capital and most populous city of France, with an area of and a population of 2,206,488.

## Parse tree

A parse tree or parsing tree or derivation tree or concrete syntax tree is an ordered, rooted tree that represents the syntactic structure of a string according to some context-free grammar.

## Partially ordered set

In mathematics, especially order theory, a partially ordered set (also poset) formalizes and generalizes the intuitive concept of an ordering, sequencing, or arrangement of the elements of a set.

## Paul Halmos

Paul Richard Halmos (Halmos Pál; March 3, 1916 – October 2, 2006) was a Hungarian-Jewish-born American mathematician who made fundamental advances in the areas of mathematical logic, probability theory, statistics, operator theory, ergodic theory, and functional analysis (in particular, Hilbert spaces).

## Peano axioms

In mathematical logic, the Peano axioms, also known as the Dedekind–Peano axioms or the Peano postulates, are axioms for the natural numbers presented by the 19th century Italian mathematician Giuseppe Peano.

## Per Lindström

Per "Pelle" Lindström (9 April 1936 – 21 August 2009, Gothenburg)ASL, September 2009 was a Swedish logician, after whom Lindström's theorem and the Lindström quantifier are named.

## Peter B. Andrews

Peter Bruce Andrews (born 1937) is an American mathematician and Professor of Mathematics, Emeritus at Carnegie Mellon University in Pittsburgh, Pennsylvania, and the creator of the mathematical logic Q0.

Philadelphia is the largest city in the U.S. state and Commonwealth of Pennsylvania, and the sixth-most populous U.S. city, with a 2017 census-estimated population of 1,580,863.

## Philosophy

Philosophy (from Greek φιλοσοφία, philosophia, literally "love of wisdom") is the study of general and fundamental problems concerning matters such as existence, knowledge, values, reason, mind, and language.

## Plural quantification

In mathematics and logic, plural quantification is the theory that an individual variable x may take on plural, as well as singular, values.

## Polish notation

Polish notation (PN), also known as normal Polish notation (NPN), Łukasiewicz notation, Warsaw notation, Polish prefix notation or simply prefix notation, is a mathematical notation in which operators precede their operands, in contrast to reverse Polish notation (RPN) in which operators follow their operands.

Polyadic algebras (more recently called Halmos algebras) are algebraic structures introduced by Paul Halmos.

## Power set

In mathematics, the power set (or powerset) of any set is the set of all subsets of, including the empty set and itself, variously denoted as, 𝒫(), ℘() (using the "Weierstrass p"),,, or, identifying the powerset of with the set of all functions from to a given set of two elements,.

## Predicate (mathematical logic)

In mathematical logic, a predicate is commonly understood to be a Boolean-valued function P: X→, called the predicate on X. However, predicates have many different uses and interpretations in mathematics and logic, and their precise definition, meaning and use will vary from theory to theory.

## Predicate functor logic

In mathematical logic, predicate functor logic (PFL) is one of several ways to express first-order logic (also known as predicate logic) by purely algebraic means, i.e., without quantified variables.

## Prenex normal form

A formula of the predicate calculus is in prenex normal form if it is written as a string of quantifiers (referred to as the prefix) followed by a quantifier-free part (referred to as the matrix).

## Prime number theorem

In number theory, the prime number theorem (PNT) describes the asymptotic distribution of the prime numbers among the positive integers.

## Principia Mathematica

The Principia Mathematica (often abbreviated PM) is a three-volume work on the foundations of mathematics written by Alfred North Whitehead and Bertrand Russell and published in 1910, 1912, and 1913.

## Principles of Mathematical Logic

Principles of Mathematical Logic is the 1950 American translation of the 1938 second edition of David Hilbert's and Wilhelm Ackermann's classic text Grundzüge der theoretischen Logik, on elementary mathematical logic.

## Projection (set theory)

In set theory, a projection is one of two closely related types of functions or operations, namely.

## Prolog

Prolog is a general-purpose logic programming language associated with artificial intelligence and computational linguistics.

## Proof assistant

In computer science and mathematical logic, a proof assistant or interactive theorem prover is a software tool to assist with the development of formal proofs by human-machine collaboration.

## Proof theory

Proof theory is a major branchAccording to Wang (1981), pp.

## Propositional calculus

Propositional calculus is a branch of logic.

## Propositional variable

In mathematical logic, a propositional variable (also called a sentential variable or sentential letter) is a variable which can either be true or false.

## Quantifier (logic)

In logic, quantification specifies the quantity of specimens in the domain of discourse that satisfy an open formula.

## Raymond Smullyan

Raymond Merrill Smullyan (May 25, 1919 – February 6, 2017) was an American mathematician, magician, concert pianist, logician, Taoist, and philosopher.

## Real line

In mathematics, the real line, or real number line is the line whose points are the real numbers.

## Recursive definition

A recursive definition (or inductive definition) in mathematical logic and computer science is used to define the elements in a set in terms of other elements in the set (Aczel 1978:740ff).

## Recursively enumerable set

In computability theory, traditionally called recursion theory, a set S of natural numbers is called recursively enumerable, computably enumerable, semidecidable, provable or Turing-recognizable if.

## Relation algebra

In mathematics and abstract algebra, a relation algebra is a residuated Boolean algebra expanded with an involution called converse, a unary operation.

## Relational algebra

Relational algebra, first created by Edgar F. Codd while at IBM, is a family of algebras with a well-founded semantics used for modelling the data stored in relational databases, and defining queries on it.

## Relational model

The relational model (RM) for database management is an approach to managing data using a structure and language consistent with first-order predicate logic, first described in 1969 by Edgar F. Codd, where all data is represented in terms of tuples, grouped into relations.

## Republic (Plato)

The Republic (Πολιτεία, Politeia; Latin: Res Publica) is a Socratic dialogue, written by Plato around 380 BC, concerning justice (δικαιοσύνη), the order and character of the just, city-state, and the just man.

## Resolution (logic)

In mathematical logic and automated theorem proving, resolution is a rule of inference leading to a refutation theorem-proving technique for sentences in propositional logic and first-order logic.

## Routledge

Routledge is a British multinational publisher.

## Rule of inference

In logic, a rule of inference, inference rule or transformation rule is a logical form consisting of a function which takes premises, analyzes their syntax, and returns a conclusion (or conclusions).

## Saint Joseph's University

Saint Joseph's University (also referred to as SJU or St. Joe's) is a private, coeducational Roman Catholic Jesuit university located in Philadelphia, Pennsylvania.

## Search algorithm

In computer science, a search algorithm is any algorithm which solves the search problem, namely, to retrieve information stored within some data structure, or calculated in the search space of a problem domain.

## Second-order arithmetic

In mathematical logic, second-order arithmetic is a collection of axiomatic systems that formalize the natural numbers and their subsets.

## Second-order logic

In logic and mathematics second-order logic is an extension of first-order logic, which itself is an extension of propositional logic.

## Semantics

Semantics (from σημαντικός sēmantikós, "significant") is the linguistic and philosophical study of meaning, in language, programming languages, formal logics, and semiotics.

## Semantics of logic

In logic, the semantics of logic is the study of the semantics, or interpretations, of formal and (idealizations of) natural languages usually trying to capture the pre-theoretic notion of entailment.

## Sentence (mathematical logic)

In mathematical logic, a sentence of a predicate logic is a boolean-valued well-formed formula with no free variables.

## Sequent calculus

Sequent calculus is, in essence, a style of formal logical argumentation where every line of a proof is a conditional tautology (called a sequent by Gerhard Gentzen) instead of an unconditional tautology.

## Set theory

Set theory is a branch of mathematical logic that studies sets, which informally are collections of objects.

## Sheffer stroke

In Boolean functions and propositional calculus, the Sheffer stroke, named after Henry M. Sheffer, written ↑, also written | (not to be confused with "||", which is often used to represent disjunction), or Dpq (in Bocheński notation), denotes a logical operation that is equivalent to the negation of the conjunction operation, expressed in ordinary language as "not both".

## Signature (logic)

In logic, especially mathematical logic, a signature lists and describes the non-logical symbols of a formal language.

## Skolem normal form

In mathematical logic, a formula of first-order logic is in Skolem normal form if it is in prenex normal form with only universal first-order quantifiers.

In mathematical logic and philosophy, Skolem's paradox is a seeming contradiction that arises from the downward Löwenheim–Skolem theorem.

## Socrates

Socrates (Sōkrátēs,; – 399 BC) was a classical Greek (Athenian) philosopher credited as one of the founders of Western philosophy, and as being the first moral philosopher, of the Western ethical tradition of thought.

## Springer Science+Business Media

Springer Science+Business Media or Springer, part of Springer Nature since 2015, is a global publishing company that publishes books, e-books and peer-reviewed journals in science, humanities, technical and medical (STM) publishing.

## Stanford Encyclopedia of Philosophy

The Stanford Encyclopedia of Philosophy (SEP) combines an online encyclopedia of philosophy with peer-reviewed publication of original papers in philosophy, freely accessible to Internet users.

## Syntax

In linguistics, syntax is the set of rules, principles, and processes that govern the structure of sentences in a given language, usually including word order.

## T-norm fuzzy logics

T-norm fuzzy logics are a family of non-classical logics, informally delimited by having a semantics that takes the real unit interval for the system of truth values and functions called t-norms for permissible interpretations of conjunction.

## T-schema

The T-schema or truth schema (not to be confused with 'Convention T') is used to give an inductive definition of truth which lies at the heart of any realisation of Alfred Tarski's semantic theory of truth.

## Tarski's World

Tarski's World is a computer-based introduction to first-order logic written by Jon Barwise and John Etchemendy.

## Tautology (logic)

In logic, a tautology (from the Greek word ταυτολογία) is a formula or assertion that is true in every possible interpretation.

## Term (logic)

In analogy to natural language, where a noun phrase refers to an object and a whole sentence refers to a fact, in mathematical logic, a term denotes a mathematical object and a formula denotes a mathematical fact.

## Theory (mathematical logic)

In mathematical logic, a theory (also called a formal theory) is a set of sentences in a formal language.

## Topology

In mathematics, topology (from the Greek τόπος, place, and λόγος, study) is concerned with the properties of space that are preserved under continuous deformations, such as stretching, crumpling and bending, but not tearing or gluing.

## Truth table

A truth table is a mathematical table used in logic—specifically in connection with Boolean algebra, boolean functions, and propositional calculus—which sets out the functional values of logical expressions on each of their functional arguments, that is, for each combination of values taken by their logical variables (Enderton, 2001).

## Truth value

In logic and mathematics, a truth value, sometimes called a logical value, is a value indicating the relation of a proposition to truth.

## Two-element Boolean algebra

In mathematics and abstract algebra, the two-element Boolean algebra is the Boolean algebra whose underlying set (or universe or carrier) B is the Boolean domain.

## Two-variable logic

In mathematical logic and computer science, two-variable logic is the fragment of first-order logic where formulae can be written using only two different variables.

## Type (model theory)

In model theory and related areas of mathematics, a type is an object that, loosely speaking, describes how a (real or possible) element or elements in a mathematical structure might behave.

## Type theory

In mathematics, logic, and computer science, a type theory is any of a class of formal systems, some of which can serve as alternatives to set theory as a foundation for all mathematics.

## Uncountable set

In mathematics, an uncountable set (or uncountably infinite set) is an infinite set that contains too many elements to be countable.

## Undergraduate Texts in Mathematics

Undergraduate Texts in Mathematics (UTM) is a series of undergraduate-level textbooks in mathematics published by Springer-Verlag.

## Uniqueness quantification

In mathematics and logic, the phrase "there is one and only one" is used to indicate that exactly one object with a certain property exists.

## Universal generalization

In predicate logic, generalization (also universal generalization or universal introduction, GEN) is a valid inference rule.

## Universal quantification

In predicate logic, a universal quantification is a type of quantifier, a logical constant which is interpreted as "given any" or "for all".

## Wedge (symbol)

Wedge (∧) is a symbol that looks similar to an in-line caret (^).

## Well-formed formula

In mathematical logic, propositional logic and predicate logic, a well-formed formula, abbreviated WFF or wff, often simply formula, is a finite sequence of symbols from a given alphabet that is part of a formal language.

## Wilfrid Hodges

Wilfrid Augustine Hodges, FBA (born 27 May 1941) is a British mathematician, known for his work in model theory.

## Wilhelm Ackermann

Wilhelm Friedrich Ackermann (29 March 1896 – 24 December 1962) was a German mathematician best known for the Ackermann function, an important example in the theory of computation.

## Willard Van Orman Quine

Willard Van Orman Quine (known to intimates as "Van"; June 25, 1908 – December 25, 2000) was an American philosopher and logician in the analytic tradition, recognized as "one of the most influential philosophers of the twentieth century." From 1930 until his death 70 years later, Quine was continually affiliated with Harvard University in one way or another, first as a student, then as a professor of philosophy and a teacher of logic and set theory, and finally as a professor emeritus who published or revised several books in retirement.

## Zermelo–Fraenkel set theory

In mathematics, Zermelo–Fraenkel set theory, named after mathematicians Ernst Zermelo and Abraham Fraenkel, is an axiomatic system that was proposed in the early twentieth century in order to formulate a theory of sets free of paradoxes such as Russell's paradox.

## References

Hey! We are on Facebook now! »