Next: About this document
CS 486 Applied Logic Assignment #6
Spring 1997 Due Date: Thurs., 3/6/97
Discuss Prelim Date: March 13 or March 27
Estimated time: less than 6 hours
- Solve the exercise on page 63 of Smullyan.
- Say that a set
with operation 
and element 
and relation < is an ordered abelian monoid iff
- is associative and commutative
- is an identity with respect to
- < is a linear order on such that
implies 
for any 
.
Write first-order relations which specify this structure. Don't forget about 
for equality.
- Take three statements from mathematics that interest you, like the definition of continuity, and specify them in first-order logic.
- Here is a statement of the theorem describing a translation from Tableau Proofs to Refinement Proofs. Class Theorem 1. For all lists of formulas
and 
if 
by a Modified Block Tableau of Smullyan (called also Gentzen tableau), then 
in Refinement Logic where 
is 
.
- Prove the case of the theorem corresponding to the rules
and 
.
- Apply the translation from your proof to these examples
-
-
.
- Write a summary of Smullyan's proof of the Godël Completeness theorem that reduces to about half a page but covers the key ideas.
- Put the following formulas into prenex form.
-
-
- Optional extra credit: Write up lecture 11 (Tuesday, February 25) on specifying finite automata.