Recent content by Mr.Cauliflower

You're right, I think I found it as Lindenbaum's lemma. Anyway, I don't know how to do this:

Could someone please help me with the proof of the following statement? Let L be language with n different constants and at least one predicate symbol. Prove that there exist 2 different maximal consistent sets formed of closed formulas of the language L.

Of course, I mean "Constants theorem" instead of "Equivalence theorem". Now I get it, thank you.

You're right, it's my typo. Thank you for help.

I think we're both saying the same, I wrote ...no subformula of form.... So the result is that I should know something more about the variables in [tex]A \rightarrow B[/itex] to know if I can directly use the axiom of specification ( = if term t can be substituted for x)? Or that I can...

Here it is, there is a note after the proof of the deduction theorem: 3.46 If A is not closed and has free variables y_1, ..., y_n, if we want to prove the implication A \rightarrow B from hypotheses T, we extend the language with new constants c_1, ..., c_n. Then T \vdash A \rightarrow...

That's a nice idea and now I maybe see why this theorem is trut, BUT I still don't get why we use it (according to my book) when we want to use the deduction theorem and the formula A is not closed (ie. it contains some free variable). I will repeat what my book says about deduction theorem...

We say that term t is substituable for variable x in formula A if for each variable y from t no subformula of A of form (\forall x) B, (\exists x) B contains free occurence of x. And if this condition is satisfied, then A_{x}[t] means formula A with ALL occurrences of x substituted...

So I suppose there's no problem having unbound x in A -> B? It would be strange if it was problem, but to be sure...

Ok, I'll try that: Let T be a set of formulas of the language L and let A be formula of the language L. Let L' be created from L extending with new symbols for constants. If c_1, ..., c_m are new constants and x_1, ..., x_m are variables then T \vdash A_{x_{1}, ..., x_{m}}[c_1, ...

Yes, I mean the hypotheses are (apart from the obvious hypothesis A) given by what I want to achieve and in that proof they show what can be deduced from those two hypotheses (it's ok to show it) and then they put it on the left side in the deduction theorem, use it and...we have exactly what we...

It's not that (\forall x)(P(x) \rightarrow Q(x)) implies that P(x) is true. Now, when (I hope) I understand it, i see the P(x) hypothesis is there because later, there is deduction theorem used and as it can be seen from the proof, it's ok I think. And truth table in predicate...

I work in first-order predicate logic and if what you mean by deduction system is a set of axioms and inference rules, those are: (axioms) A \rightarrow (B \rightarrow A) (A \rightarrow (B \rightarrow C)) \rightarrow ((A \rightarrow B) \rightarrow (A \rightarrow C))...

Thank you. Could you tell me the name you use for the axiom I used here? I often don't know how to translate these things from Czech to English when I want to find something on Google.

Hello, I wonder whether if I have this formula to prove: (\forall x)(P(x) \rightarrow Q(x)) \rightarrow ((\forall x) P(x) \rightarrow (\forall x) Q(x)) is it correct to have both (\forall x)(P(x) \rightarrow Q(x)) and ((\forall x) P(x) as hypotheses in the proof...