207 relations: Abelian group, Abstract algebra, ACL2, Alan Turing, Alfred Tarski, Algebra, Alonzo Church, Amsterdam, Arithmetic, Arity, Atomic formula, Atomic sentence, Automated proof checking, Automated theorem proving, Axiom, Axiom of choice, Axiom of empty set, Axiom of extensionality, Axiom schema, Axiomatic system, Ben Goertzel, Bernays–Schönfinkel class, Binary relation, Boolean-valued function, Bounded quantifier, Branching quantifier, Cardinal number, Cardinality, Central processing unit, Charles Sanders Peirce, Compactness theorem, Complete theory, Completeness (logic), Computational complexity theory, Computer science, Congruence relation, Connected component (graph theory), Consistency, Context-free grammar, Countable set, Cylindric algebra, Data type, David Hilbert, Decidability (logic), Decision problem, Description logic, Directed graph, Domain of discourse, Dover Publications, Elementary class, ..., Empty set, Entscheidungsproblem, Equiconsistency, Equivalence relation, Exclusive or, Existential quantification, Extension by definitions, Formal grammar, Formal language, Formal specification, Formal system, Formal verification, Formation rule, Foundations of mathematics, Free logic, Gödel's completeness theorem, Gödel's incompleteness theorems, George Boolos, George Edward Hughes, Gottlob Frege, Graph (discrete mathematics), Group (mathematics), Guarded logic, Halting problem, Heinz-Dieter Ebbinghaus, Herbrandization, Heuristic (computer science), Higher-order logic, Hilbert system, Interpretation (logic), Intuitionistic logic, Isabelle (proof assistant), Józef Maria Bocheński, John Etchemendy, Jon Barwise, Kurt Gödel, L. T. F. Gamut, Lattice (order), Löwenheim number, Löwenheim–Skolem theorem, Lindenbaum–Tarski algebra, Lindström's theorem, Linguistics, List of first-order theories, List of logic symbols, Logic of graphs, Logical biconditional, Logical conjunction, Logical connective, Logical consequence, Logical disjunction, Logical equality, Logical NOR, London, Material conditional, Mathematical proof, Mathematics, Max Cresswell, Metalogic, Metamath, Method of analytic tableaux, Mizar system, Modal logic, Model theory, Modus ponens, Monadic predicate calculus, Morley's categoricity theorem, Natural deduction, Natural number, Negation, New York City, Non-logical symbol, Non-standard model, Nonfirstorderizability, Number theory, Order of operations, Ordered field, Ordered pair, Pairing function, Paris, Parse tree, Partially ordered set, Paul Halmos, Peano axioms, Per Lindström, Peter B. Andrews, Philadelphia, Philosophy, Plural quantification, Polish notation, Polyadic algebra, Power set, Predicate (mathematical logic), Predicate functor logic, Prenex normal form, Prime number theorem, Principia Mathematica, Principles of Mathematical Logic, Projection (set theory), Prolog, Proof assistant, Proof theory, Propositional calculus, Propositional variable, Quantifier (logic), Raymond Smullyan, Real line, Recursive definition, Recursively enumerable set, Relation algebra, Relational algebra, Relational model, Republic (Plato), Resolution (logic), Routledge, Rule of inference, Saint Joseph's University, Search algorithm, Second-order arithmetic, Second-order logic, Semantics, Semantics of logic, Sentence (mathematical logic), Sequent calculus, Set theory, Sheffer stroke, Signature (logic), Skolem normal form, Skolem's paradox, Socrates, Springer Science+Business Media, Stanford Encyclopedia of Philosophy, Syntax, T-norm fuzzy logics, T-schema, Tarski's World, Tautology (logic), Term (logic), Theory (mathematical logic), Topology, Truth table, Truth value, Two-element Boolean algebra, Two-variable logic, Type (model theory), Type theory, Uncountable set, Undergraduate Texts in Mathematics, Uniqueness quantification, Universal generalization, Universal quantification, Wedge (symbol), Well-formed formula, Wilfrid Hodges, Wilhelm Ackermann, Willard Van Orman Quine, Zermelo–Fraenkel set theory. Expand index (157 more) » « Shrink index
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.
In algebra, which is a broad division of mathematics, abstract algebra (occasionally called modern algebra) is the study of algebraic structures.
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 Mathison Turing (23 June 1912 – 7 June 1954) was an English computer scientist, mathematician, logician, cryptanalyst, philosopher, and theoretical biologist.
Alfred Tarski (January 14, 1901 – 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 (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 (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 is the capital and most populous municipality of the Netherlands.
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.
In logic, mathematics, and computer science, the arity of a function or operation is the number of arguments or operands that the function takes.
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.
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 is the process of using software for checking proofs for correctness.
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.
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.
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.
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.
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.
In mathematical logic, an axiom schema (plural: axiom schemata or axiom schemas) generalizes the notion of axiom.
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 (born December 8, 1966) is the founder and CEO of SingularityNET, a blockchain-based AI marketplace.
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.
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.
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.
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 "∃".
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 ∈.
In mathematics, cardinal numbers, or cardinals for short, are a generalization of the natural numbers used to measure the cardinality (size) of sets.
In mathematics, the cardinality of a set is a measure of the "number of elements of the set".
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 ("purse"; 10 September 1839 – 19 April 1914) was an American philosopher, logician, mathematician, and scientist who is sometimes known as "the father of pragmatism".
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.
In mathematical logic, a theory is complete if, for every formula in the theory's language, that formula or its negation is demonstrable.
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 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 deals with the theoretical foundations of information and computation, together with practical techniques for the implementation and application of these foundations.
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.
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.
In classical deductive logic, a consistent theory is one that does not contain a contradiction.
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.
In mathematics, a countable set is a set with the same cardinality (number of elements) as some subset of the set of natural numbers.
The notion of cylindric algebra, invented by Alfred Tarski, arises naturally in the algebraization of equational first-order logic.
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 (23 January 1862 – 14 February 1943) was a German mathematician.
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).
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 logics (DL) are a family of formal knowledge representation languages.
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.
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, also known as Dover Books, is an American book publisher founded in 1941 by Hayward Cirker and his wife, Blanche.
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.
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.
In mathematics and computer science, the Entscheidungsproblem (German for "decision problem") is a challenge posed by David Hilbert in 1928.
In mathematical logic, two theories are equiconsistent if the consistency of one theory implies the consistency of the other theory, and vice versa.
In mathematics, an equivalence relation is a binary relation that is reflexive, symmetric and transitive.
Exclusive or or exclusive disjunction is a logical operation that outputs true only when inputs differ (one is true, the other is false).
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".
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.
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.
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.
In computer science, formal specifications are mathematically based techniques whose purpose are to help with the implementation of systems and software.
A formal system is the name of a logic system usually defined in the mathematical way.
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.
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 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.
A free logic is a logic with fewer existential presuppositions than classical logic.
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 are two theorems of mathematical logic that demonstrate the inherent limitations of every formal axiomatic system containing basic arithmetic.
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 (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.
Friedrich Ludwig Gottlob Frege (8 November 1848 – 26 July 1925) was a German philosopher, logician, and mathematician.
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".
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 is a choice set of dynamic logic involved in choices, where outcomes are limited.
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 (born 22 February 1939 in Hemer, Province of Westphalia) is a German mathematician and logician.
The Herbrandization of a logical formula (named after Jacques Herbrand) is a construction that is dual to the Skolemization of a formula.
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.
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.
In logic, especially mathematical logic, a Hilbert system, sometimes called Hilbert calculus, Hilbert-style deductive system or Hilbert–Ackermann system, is a type of system of formal deduction attributed to Gottlob FregeMáté & Ruzsa 1997:129 and David Hilbert.
An interpretation is an assignment of meaning to the symbols of a formal language.
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.
The Isabelle theorem prover is an interactive theorem prover, a Higher Order Logic (HOL) theorem prover.
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 W. Etchemendy (born 1952 in Reno, Nevada) was Stanford University's twelfth Provost.
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 Friedrich Gödel (April 28, 1906 – January 14, 1978) was an Austrian, and later American, logician, mathematician, and philosopher.
A lattice is an abstract structure studied in the mathematical subdisciplines of order theory and abstract algebra.
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.
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.
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).
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 is the scientific study of language, and involves an analysis of language form, language meaning, and language in context.
In mathematical logic, a first-order theory is given by a set of axioms in some language.
In logic, a set of symbols is commonly used to express logical representation.
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.
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.
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.
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 (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.
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 is a logical operator that corresponds to equality in Boolean algebra and to the logical biconditional in propositional calculus.
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 is the capital and most populous city of England and the United Kingdom.
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 "→".
In mathematics, a proof is an inferential argument for a mathematical statement.
Mathematics (from Greek μάθημα máthēma, "knowledge, study, learning") is the study of such topics as quantity, structure, space, and change.
Maxwell John Cresswell (born 19 November 1939, Wellington) is a New Zealand philosopher and logician, known for his work in modal logic.
Metalogic is the study of the metatheory of logic.
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.
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.
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 is a type of formal logic primarily developed in the 1960s that extends classical propositional and predicate logic to include operators expressing modality.
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.
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.
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.
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.
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.
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").
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.
The City of New York, often called New York City (NYC) or simply New York, is the most populous city in the United States.
In logic, the formal languages used to create expressions consist of symbols, which can be broadly divided into constants and variables.
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).
In formal logic, nonfirstorderizability is the inability of an expression to be adequately captured in particular theories in first-order logic.
Number theory, or in older usage arithmetic, is a branch of pure mathematics devoted primarily to the study of the integers.
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.
In mathematics, an ordered field is a field together with a total ordering of its elements that is compatible with the field operations.
In mathematics, an ordered pair (a, b) is a pair of objects.
In mathematics, a pairing function is a process to uniquely encode two natural numbers into a single natural number.
Paris is the capital and most populous city of France, with an area of and a population of 2,206,488.
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.
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 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).
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 "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 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 (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.
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 (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.
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,.
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.
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.
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).
In number theory, the prime number theorem (PNT) describes the asymptotic distribution of the prime numbers among the positive integers.
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 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.
In set theory, a projection is one of two closely related types of functions or operations, namely.
Prolog is a general-purpose logic programming language associated with artificial intelligence and computational linguistics.
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 is a major branchAccording to Wang (1981), pp.
Propositional calculus is a branch of logic.
In mathematical logic, a propositional variable (also called a sentential variable or sentential letter) is a variable which can either be true or false.
In logic, quantification specifies the quantity of specimens in the domain of discourse that satisfy an open formula.
Raymond Merrill Smullyan (May 25, 1919 – February 6, 2017) was an American mathematician, magician, concert pianist, logician, Taoist, and philosopher.
In mathematics, the real line, or real number line is the line whose points are the real numbers.
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).
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.
In mathematics and abstract algebra, a relation algebra is a residuated Boolean algebra expanded with an involution called converse, a unary operation.
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.
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.
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.
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 is a British multinational publisher.
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 (also referred to as SJU or St. Joe's) is a private, coeducational Roman Catholic Jesuit university located in Philadelphia, Pennsylvania.
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.
In mathematical logic, second-order arithmetic is a collection of axiomatic systems that formalize the natural numbers and their subsets.
In logic and mathematics second-order logic is an extension of first-order logic, which itself is an extension of propositional logic.
Semantics (from σημαντικός sēmantikós, "significant") is the linguistic and philosophical study of meaning, in language, programming languages, formal logics, and semiotics.
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.
In mathematical logic, a sentence of a predicate logic is a boolean-valued well-formed formula with no free variables.
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 is a branch of mathematical logic that studies sets, which informally are collections of objects.
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".
In logic, especially mathematical logic, a signature lists and describes the non-logical symbols of a formal language.
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 (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 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.
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.
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 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.
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 is a computer-based introduction to first-order logic written by Jon Barwise and John Etchemendy.
In logic, a tautology (from the Greek word ταυτολογία) is a formula or assertion that is true in every possible interpretation.
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.
In mathematical logic, a theory (also called a formal theory) is a set of sentences in a formal language.
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.
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).
In logic and mathematics, a truth value, sometimes called a logical value, is a value indicating the relation of a proposition to truth.
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.
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.
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.
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.
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 (UTM) is a series of undergraduate-level textbooks in mathematics published by Springer-Verlag.
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.
In predicate logic, generalization (also universal generalization or universal introduction, GEN) is a valid inference rule.
In predicate logic, a universal quantification is a type of quantifier, a logical constant which is interpreted as "given any" or "for all".
Wedge (∧) is a symbol that looks similar to an in-line caret (^).
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 Augustine Hodges, FBA (born 27 May 1941) is a British mathematician, known for his work in model theory.
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 (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.
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.
1st order logic, Classical predicate logic, Deductive systems for first-order logic, Equational first-order logic, FOPC, FOPL, First Order Language, First Order Logic, First order language, First order logic, First order logic with equality, First order predicate calculus, First order predicate logic, First-Order Logic, First-order Peano arithmetic, First-order language, First-order logic with equality, First-order predicate calculus, First-order predicate logic, First-order sentence, First-order theory, First-order-logic, Fixpoint logic, Lower Predicate Calculus, Many-sorted first-order logic, Polyadic predicate calculus, Predicate Calculus, Predicate Logic, Predicate calculus, Predicate logic, Predicate logic (Philosophy), Predicate logic (philosophy), Quantification calculus, Quantification theory, Semantics of first-order logic, Tarskian semantics.