Revision as of 21:29, 27 April 2003 edit Toby Bartels (talk \| contribs) Administrators 8,880 edits m Help search engine. ← Previous edit		Revision as of 21:41, 27 April 2003 edit undo Toby Bartels (talk \| contribs) Administrators 8,880 edits m Typos. Next edit →
Line 10: Then <i>F</i> can be modelled by the set : [<i>F</i>] := {([<i>X</i>],[<i>F</i>(<i>X</i>)]) : [<i>X</i>] in [<b>T</b>]}, which is simply a [[function]] with ___domain [<b>T</b>] and codomain [<b>U</b>]. It is a requirement of a consistent model that [<i>F</i>(<i>X</i>)] = [<i>F</i>(<i>Y</i>)] whenever [<i>X</i>] = [<i>Y</i>]. Line 20: One also gets certain function symbols automatically. ~~Given~~In ~~any~~untyped ~~type <b>T</b>~~logic, there is anin ''identity predicate'' id~~<sub><b>T</b></sub> with ___domain and codomain type <b>T</b>;~~ itthat satisfies id~~<sub><b>T</b></sub>~~(<i>X</i>) = <i>X</i> for all <i>X</i~~> of type <b>T</b~~>. In typed logic, given any type <b>T</b>, there is an identity predicate id<sub><b>T</b></sub> with ___domain and codomain type <b>T</b>; it satisfies id<sub><b>T</b></sub>(<i>X</i>) = <i>X</i> for all <i>X</i> of type <b>T</b>. Similarly, if <b>T</b> is a [[subtype]] of <b>U</b>, then there is an inclusion predicate of ___domain type <b>T</b> and codomain type <b>U</b> that satisfies the same equation; there are additional function symbols associated with other ways of constructing new types out of old ones. Line 36 ⟶ 37: Many treatments of predicate logic don't allow functional predicates, only relational [[predicate (logic)\|predicate]]s. This is useful, for example, in the context of proving [[metalogic]]al theorems (such as [[Gödel's incompleteness theorem]]s), where one doesn't want to allow the introduction of new functional symbols (nor any other new symbols, for that matter). But there is a method of replacing functional symbols with relational ~~sybmols~~symbols wherever the former may occur; furthermore, this is algorithmic and thus suitable for applying most metalogical theorems to the result. Specifically, if <i>F</i> has ___domain type <b>T</b> and codomain type <b>U</b>, then it can be replaced with a predicate <i>P</i> of type (<b>T</b>,<b>U</b>). Line 54 ⟶ 55: (This example uses [[mathematical symbols]].) This schema states (in one form), for any functional predicate <i>F</i> in one variable: : ∀ <i>A</i>, ∃ <i>B</i>, ∀ <i>C</i>, <i>C</i> ∈ <i>A</i> → <i>F</i>(<i>C</i>) ∈ <i>B</i>. ~~First~~F irst, we must replace <i>F</i>(<i>C</i>) with some other variable <i>D</i>: :∀ <i>A</i>, ∃ <i>B</i>, ∀ <i>C</i>, <i>C</i> ∈ <i>A</i> → <i>D</i> ∈ <i>B</i>. Of course, this statment isn't correct; <i>D</i> must be quantified over just after <i>C</i>: : ∀ <i>A</i>, ∃ <i>B</i>, ∀ <i>C</i>, ∀ <i>D</i>, <i>C</i> ∈ <i>A</i> → <i>D</i> ∈ <i>B</i>. We still must introduce <i>P</i> to guard this quantification: : ∀ <i>A</i>, ∃ <i>B</i>, ∀ <i>C</i>, ∀ <i>D</i>, <i>P</i>(<i>C</i>,<i>D</i>) → (<i>C</i> ∈ <i>A</i> → <i>D</i> ∈ <i>B</i>). This is almost correct, but it ~~applying~~applies to too many predicates; what we actually want is: : (∀ <i>X</i>, ∃! <i>Y</i>, <i>P</i>(<i>X</i>,<i>Y</i>)) → (∀ <i>A</i>, ∃ <i>B</i>, ∀ <i>C</i>, ∀ <i>D</i>, <i>P</i>(<i>C</i>,<i>D</i>) → (<i>C</i> ∈ <i>A</i> → <i>D</i> ∈ <i>B</i>)). This version of the axiom schema of replacement is now suitable for use in a formal language that doesn't allow the introduction of new function symbols. Alternatively, one may interpret the original statement as a statement in such a formal language; it was merely an abbreviation for the statement produced at the end.

Functional predicate: Difference between revisions