[mathematical logic] predicate logic (first-order predicate logic formula | example)

Last blog : 【 Mathematical logic 】 Predicate logic ( Individual words | Individual domain | The predicate | Full name quantifier | There are quantifiers | Predicate formula | exercises )

One 、 First order predicate logic formula

---

Propositional formula : Basic proposition ( Propositional constant / Argument ) and A number of Conjunctions Form a finite length string ;

① Single Propositional argument / Propositional constant Is a proposition formula ;

② If

A

A

A Is a proposition formula , be

(

¬

A

)

(\lnot A)

(¬A) It is also a propositional formula ;

③ If

A

,

B

A,B

A,B Is a proposition formula , be

(

A

∧

B

)

,

(

A

∨

B

)

,

(

A

→

B

)

,

(

A

B

)

(A \land B) , (A \lor B), (A \to B), (A \leftrightarrow B)

(A∧B),(A∨B),(A→B),(AB) It is also a propositional formula ;

④ A limited number of times application ① ② ③ Formed symbol string Is a proposition formula ; ( Infinite times cannot )

First order predicate logic formula : stay Propositional formula On the basis of , Add a condition :

If

A

A

A It's the formula , be

∀

x

A

\forall x A

∀xA and

∃

x

A

\exist x A

∃xA Is also a formula

Related concepts of first-order predicate logic formula : With

∀

x

A

\forall x A

∀xA ,

∃

x

A

\exist x A

∃xA Take the formula as an example ;

Guide arguments :

∀

,

∃

\forall , \exist

∀,∃ After quantifier

x

x

x be called Guide arguments

Jurisdiction :

A

A

A be called The scope of the corresponding quantifier ;

Constraints appear : stay

∀

x

\forall x

∀x ,

∃

x

\exist x

∃x Jurisdiction

A

A

A in ,

x

x

x All appearances are constrained , This is called constraint occurrence ;

Free to appear : Jurisdiction

A

A

A in , It is not the argument of the constraint , Are free to appear ;

Two 、 First order predicate logic formula Example

---

First order predicate logic formula :

∀

x

(

F

(

x

)

→

∃

y

(

G

(

y

)

∧

H

(

x

,

y

,

z

)

)

)

\forall x ( F(x) \to \exist y ( G(y) \land H(x,y,z) ) )

∀x(F(x)→∃y(G(y)∧H(x,y,z)))

Formula interpretation : about All satisfied

F

F

F Nature

x

x

x , all There is satisfaction

G

G

G The object of nature

y

y

y , bring

x

,

y

,

z

x,y,z

x,y,z Satisfaction

H

H

H ;

∀

x

\forall x

∀x Of Jurisdiction yes

(

F

(

x

)

→

∃

y

(

G

(

y

)

∧

H

(

x

,

y

,

z

)

)

)

( F(x) \to \exist y ( G(y) \land H(x,y,z) ) )

(F(x)→∃y(G(y)∧H(x,y,z)))

∃

y

\exist y

∃y Of Jurisdiction yes

(

G

(

y

)

∧

H

(

x

,

y

,

z

)

)

)

( G(y) \land H(x,y,z) ) )

(G(y)∧H(x,y,z)))

x

,

y

x , y

x,y After the quantifier , yes Guide arguments , yes Constraints appear Argument of ;

z

z

z Not after the quantifier , yes Free to appear Argument of ;

Guide arguments Similar to the predefined Variable / Parameters , Free to appear Argument of It's equivalent to Temporary variable ,