• English only

# Differences

This shows you the differences between two versions of the page.

sav08:first-order_logic_is_undecidable [2008/04/03 12:58]
vkuncak
sav08:first-order_logic_is_undecidable [2008/04/03 12:59] (current)
vkuncak
Line 27: Line 27:
((\$\lnot F\$) is true in some Herbrand model) iff (\$M\$ does not accept \$w\$) ((\$\lnot F\$) is true in some Herbrand model) iff (\$M\$ does not accept \$w\$)

-So, we work with formula \$G\$ denoting \$\lnot F\$, interpreted over Herbrand model, and we express the condition that all Turing machine computation histories are non-accepting.+So, we work with formula \$G\$ denoting \$\lnot F\$, interpreted over Herbrand model, and we express the condition that all Turing machine computation histories are non-accepting.  In other words, \$F\$, when interpreted over Herbrand interpretations,​ says that there exists an accepting Turing computation history.

The fact that we work over Herbrand models helps us talk about computation histories, because we can encode strings and reachability. The fact that we work over Herbrand models helps us talk about computation histories, because we can encode strings and reachability.