Open formula: Difference between revisions

From Wikipedia, the free encyclopedia
Jump to navigation Jump to search
imported>Assem Khidhr
Importing Wikidata short description: "Formula that contains at least one free variable"
 
imported>Heavy Grasshopper
add sections
 
(One intermediate revision by one other user not shown)
Line 1: Line 1:
{{Short description|Formula that contains at least one free variable}}
{{Multiple issues| {{more categories|date=November 2025}}
{{unsourced|date=November 2025}}
{{no footnotes|date=November 2025}}}}{{Short description|Formula that contains at least one free variable}}
An '''open formula''' is a [[formula (logic)|formula]] that contains at least one [[free variable]].{{citation needed|date=September 2016}}
An '''open formula''' is a [[formula (logic)|formula]] that contains at least one [[free variable]].{{citation needed|date=September 2016}}
 
==Definition and uses==
An open formula does not have a [[truth value]] assigned to it, in contrast with a [[sentence (logic)|closed formula]] which constitutes a proposition and thus can have a truth value like ''true'' or ''false''. An open formula can be transformed into a closed formula by applying a quantifier for each free variable. This transformation is called capture of the free variables to make them bound variables.
An open formula does not have a [[truth value]] assigned to it, in contrast with a [[sentence (logic)|closed formula]] which constitutes a proposition and thus can have a truth value like ''true'' or ''false''. An open formula can be transformed into a closed formula by applying a quantifier for each free variable. This transformation is called capture of the free variables to make them bound variables.


Line 8: Line 10:
Open formulas are often used in rigorous mathematical definitions of properties, like  
Open formulas are often used in rigorous mathematical definitions of properties, like  
:"''x'' is an aunt of ''y'' if, for some person ''z'', ''z'' is a parent of ''y'', and ''x'' is a sister of ''z''"
:"''x'' is an aunt of ''y'' if, for some person ''z'', ''z'' is a parent of ''y'', and ''x'' is a sister of ''z''"
(with free variables ''x'', ''y'', and bound variable ''z'') defining the notion of "aunt" in terms of "parent" and "sister".
(with free variables ''x'', ''y'', and bound variable ''z'') defining the notion of "aunt" in terms of "parent" and "sister". Another, more formal example, which defines the property of being a [[prime number]], is  
Another, more formal example, which defines the property of being a [[prime number]], is  
:"''P''(''x'') if ∀''m'',''n''∈<math>\mathbb{N}</math>: ''m''>1 ∧ ''n''>1 → ''x''≠ ''m''⋅''n''",
:"''P''(''x'') if ∀''m'',''n''∈<math>\mathbb{N}</math>: ''m''>1 ∧ ''n''>1 → ''x''≠ ''m''⋅''n''",
(with free variable ''x'' and bound variables ''m'',''n'').
(with free variable ''x'' and bound variables ''m'',''n'').
 
==Fermat example==
An example of a closed formula with truth value ''false'' involves the sequence of [[Fermat number]]s
An example of a closed formula with truth value ''false'' involves the sequence of [[Fermat number]]s


Line 18: Line 19:


studied by Fermat in connection to the primality. The attachment of the predicate letter P (''is prime'') to each number from the Fermat sequence gives a set of closed formulae. While they are true for ''n'' = 0,...,4, no larger value of ''n'' is known that obtains a true formula, {{as of|2023|lc=y}}; for example, <math>F_5 = 4 \,294 \,967 \,297 = 641 \cdot 6\,700\,417</math> is not a prime. Thus the closed formula ∀''n'' ''P''(''F''<sub>''n''</sub>) is false.
studied by Fermat in connection to the primality. The attachment of the predicate letter P (''is prime'') to each number from the Fermat sequence gives a set of closed formulae. While they are true for ''n'' = 0,...,4, no larger value of ''n'' is known that obtains a true formula, {{as of|2023|lc=y}}; for example, <math>F_5 = 4 \,294 \,967 \,297 = 641 \cdot 6\,700\,417</math> is not a prime. Thus the closed formula ∀''n'' ''P''(''F''<sub>''n''</sub>) is false.
In [[database theory]], when expressing a query as an open [[first-order formula]], the free variables represent the ones that in an [[SQL]] query would occur in the [[Select (SQL)|SELECT]] clause. For example, a formula like:
:<math>\varphi(son) = birthYear(son,2020) \land \exists mom\textbf{.}(motherOf(mom,son) \land birthYear(mom,1999))</math>
where <math>son</math> is the only free variable, could be expressed in SQL as follows:
<syntaxhighlight lang="sql">
SELECT y1.person AS son
FROM birth_year y1
WHERE y1.year = 2020
AND EXISTS (
  SELECT *
  FROM mother_of m1
  JOIN birth_year y2 ON m1.mother = y2.person
  WHERE m1.son = y1.person
  AND y2.year = 1999
)
</syntaxhighlight>
which selects all the people born in 2020 and having a mother born in 1999.
Formally, executing the above SQL query over a database is equivalent to look for all the [[Substitution (logic)|substitutions]] <math>\sigma</math> of the free variables of <math>\varphi</math> with constants such that the [[Herbrand interpretation]] of <math>\mathcal{D}</math> [[Satisfaction (logic)|satisfies]] <math>\sigma(\varphi)</math>, where <math>\mathcal{D}</math> is the set of [[ground atom]]s representing the database.


== See also ==
== See also ==
Line 38: Line 61:


[[Category:Logical expressions]]
[[Category:Logical expressions]]
{{mathlogic-stub}}

Latest revision as of 11:26, 4 December 2025

Script error: No such module "Unsubst".Template:Short description An open formula is a formula that contains at least one free variable.Script error: No such module "Unsubst".

Definition and uses

An open formula does not have a truth value assigned to it, in contrast with a closed formula which constitutes a proposition and thus can have a truth value like true or false. An open formula can be transformed into a closed formula by applying a quantifier for each free variable. This transformation is called capture of the free variables to make them bound variables.

For example, when reasoning about natural numbers, the formula "x+2 > y" is open, since it contains the free variables x and y. In contrast, the formula "y x: x+2 > y" is closed, and has truth value true.

Open formulas are often used in rigorous mathematical definitions of properties, like

"x is an aunt of y if, for some person z, z is a parent of y, and x is a sister of z"

(with free variables x, y, and bound variable z) defining the notion of "aunt" in terms of "parent" and "sister". Another, more formal example, which defines the property of being a prime number, is

"P(x) if ∀m,n: m>1 ∧ n>1 → xmn",

(with free variable x and bound variables m,n).

Fermat example

An example of a closed formula with truth value false involves the sequence of Fermat numbers

Fn=22n+1,

studied by Fermat in connection to the primality. The attachment of the predicate letter P (is prime) to each number from the Fermat sequence gives a set of closed formulae. While they are true for n = 0,...,4, no larger value of n is known that obtains a true formula, since 2023Template:Dated maintenance category (articles)Script error: No such module "Check for unknown parameters".; for example, F5=4294967297=6416700417 is not a prime. Thus the closed formula ∀n P(Fn) is false.

In database theory, when expressing a query as an open first-order formula, the free variables represent the ones that in an SQL query would occur in the SELECT clause. For example, a formula like:

φ(son)=birthYear(son,2020)mom.(motherOf(mom,son)birthYear(mom,1999))

where son is the only free variable, could be expressed in SQL as follows:

SELECT y1.person AS son
FROM birth_year y1
WHERE y1.year = 2020
AND EXISTS (
  SELECT *
  FROM mother_of m1
  JOIN birth_year y2 ON m1.mother = y2.person
  WHERE m1.son = y1.person
  AND y2.year = 1999
)

which selects all the people born in 2020 and having a mother born in 1999.

Formally, executing the above SQL query over a database is equivalent to look for all the substitutions σ of the free variables of φ with constants such that the Herbrand interpretation of 𝒟 satisfies σ(φ), where 𝒟 is the set of ground atoms representing the database.

See also

References

<templatestyles src="Reflist/styles.css" />

Script error: No such module "Check for unknown parameters".

  • Script error: No such module "citation/CS1".
  • Script error: No such module "citation/CS1".

Template:Mathematical logic