First-order logic - Revision history

Karl Jones: /* External links */

2016-04-20T15:35:24Z

‎External links

Karl Jones: /* External links */

2016-04-12T11:59:11Z

‎External links

Karl Jones: /* See also */

2016-03-10T15:17:18Z

‎See also

Karl Jones: /* See also */

2016-03-10T15:16:56Z

‎See also

Karl Jones at 15:09, 10 March 2016

2016-03-10T15:09:52Z

Karl Jones at 15:05, 10 March 2016

2016-03-10T15:05:46Z

Karl Jones: Created page with "'''First-order logic''' is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. It is also kno..."

2016-03-10T15:05:17Z

Created page with "'''First-order logic''' is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. It is also kno..."

New page

'''First-order logic''' is a collection of [[Formal system|formal systems]] 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.

== Description ==

First-order logic uses quantified variables over (non-logical) objects.

It allows the use of sentences that contain variables, so that rather than propositions such as ''[[Socrates]] is a man'' one can have expressions in the form X is a man where X is a variable.

This distinguishes it from [[propositional logic]], which does not use quantifiers.

A theory about a topic is usually a first-order logic together with a specified domain of discourse over which the quantified variables range, finitely many functions from that domain to itself, finitely many predicates defined on that domain, and a set of axioms 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 which are both 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]].

[[Peano arithmetic]] and [[Zermelo–Fraenkel set theory]] are axiomatizations of [[number theory]] and [[set theory]], respectively, into first-order logic.

No first-order theory, however, has the strength to uniquely describe a structure with an infinite domain, such as the [[Natural number|natural numbers]] or the [[real line]].

Axioms systems that do fully describe these two structures (that is, categorical axiom systems) can be obtained in stronger logics such as [[second-order logic]].

== See also ==

* [[Logic]]
* [[Mathematics]]

== External links ==

* [https://en.wikipedia.org/wiki/First-order_logic First-order logic] @ Wikipedia

← Older revision		Revision as of 15:35, 20 April 2016
Line 65:		Line 65:

	[[Category:Logic]]		[[Category:Logic]]
		+	[[Category:Mathematics]]
		+	[[Category:Philosophy]]

← Older revision		Revision as of 11:59, 12 April 2016
Line 63:		Line 63:

	* [https://en.wikipedia.org/wiki/First-order_logic First-order logic] @ Wikipedia		* [https://en.wikipedia.org/wiki/First-order_logic First-order logic] @ Wikipedia
		+
		+	[[Category:Logic]]

@@ Line 35: / Line 35: @@
 * [[ACL2]] - computational logic for Applicative Common Lisp
 * [[Computer science]]
-* [[Equiconsistency
+* [[Equiconsistency]]
 * [[Extension by definitions]]
 * [[Formal system]]

@@ Line 33: / Line 33: @@
 == See also ==
 * [[Computer science]]
 * [[Formal system]]
 * [[Foundations of mathematics]]
 * [[Logic]]
 * [[Mathematics]]
 * [[Number theory]]
 * [[Peano arithmetic]]
 * [[Philosophy]]
 * [[Second-order logic]]
 * [[Set theory]]
 * [[Zermelo–Fraenkel set theory]]