Tell me more ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.
up vote 2 down vote favorite

Let $y$ be Godel number of some formula which is derivable in some first-order logic. $F(y,n)$ is true if and only if the number of usage $Gen$(universal generalization) inference rule in any derivation of that formula is less or equal to $n$.

Please help to show that $F(y,n)$ is recursive function. A hint or link to such proofs will be highly appreciated.

share|improve this question
1  
What if the formula with Gödel number $y$ can't be derived? What if it can but (as will in fact always be the case) there are different proofs, with different numbers of generalizations? – Chris Eagle Jan 13 at 11:13
@ChrisEagle see updated version – Ashot Jan 13 at 16:54
@Ashot That still won't work: for any $n$, any theorem has a derivation with more than $n$ uses of $Gen$. Also $F$ is a relation, so trivially isn't a recursive function. And it can't be a recursive relation either as it isn't even defined for when $y$ numbers a non-theorem. – Peter Smith Jan 13 at 17:01
My guess is that the solution involves knowing enough proof theory to manage the proofs - perhaps they need to be in cut free form. But, as a start, I would suggest taking the specific set of inference rules you are working with and proving a special case: the set of $\phi$ that are provable with no uses of generalization is decidable. – Carl Mummert Jan 14 at 12:35
@Peter Smith: I read the question as: the relation $F(\phi,n)$ holds if there exists a proof of $\phi$ using $n$ or fewer applications of generalization. Prove that $F$ is decidable. If $\psi$ is not provable then $F(\psi,n)$ is simply false for all $n$. – Carl Mummert Jan 14 at 12:37
show 5 more comments

Know someone who can answer? Share a link to this question via email, Google+, Twitter, or Facebook.

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Browse other questions tagged or ask your own question.