first order logic

A logic is first order if it has exactly one type. Usually the term refers specifically to the logic with connectivesMathworldPlanetmath ¬, , , , and and the quantifiersMathworldPlanetmath and , all given the usual semantics:

  • ¬ϕ is true iff ϕ is not true

  • ϕψ is true if either ϕ is true or ψ is true

  • xϕ(x) is true iff ϕxt is true for every object t (where ϕxt is the result of replacing every unbound occurrence of x in ϕ with t)

  • ϕψ is the same as ¬(¬ϕ¬ψ)

  • ϕψ is the same as (¬ϕ)ψ

  • ϕψ is the same as (ϕψ)(ψϕ)

  • xϕ(x) is the same as ¬x¬ϕ(x)

However languagesPlanetmathPlanetmath with slightly different quantifiers and connectives are sometimes still called first order as long as there is only one type.

Title first order logic
Canonical name FirstOrderLogic
Date of creation 2013-03-22 13:00:06
Last modified on 2013-03-22 13:00:06
Owner Henry (455)
Last modified by Henry (455)
Numerical id 7
Author Henry (455)
Entry type Definition
Classification msc 03B10
Synonym classical first order logic
Synonym FO