Logic, proving theorem in formal system K

In summary, the conversation discusses a problem involving a well formed formula in a language and an individual constant. It is trying to prove that a certain formula is a theorem of a formal system, using a proof from a link provided. However, the use of free variables and the chosen formal system make it difficult to follow the given proof.
  • #1
Barioth
49
0
Hi

here is the problem I'm working on,

Let $A(x_1)$ be a well formed formula of a language $L$ in which $x_1$ is free, let $a_1$ an invidual constant of $L$, Show that the formula $A(a_1)\rightarrow(\exists x_1)A(x_1)$ is a theorem of $K_L$

on this link, the first slide as the axiom of $K_L$

http://www.idi.ntnu.no/emner/tdt4135/handouts/slides-9.pdf

I wanted to use the following proof:

$A(a_1)\rightarrow(\exists x_1)A(x_1)$

is equivalent logic to

$(\exists x_1)(A(a_1)\rightarrow A(x_1))$

wich is equivalent logic to

$(\forall x_1)A(a_1)\rightarrow A(x_1)$

then trying to conclude using (K5) from the pdf link,

but I just realized that since $x_1$ is free in A, I cannot move the quantifier like I did.
 
Physics news on Phys.org
  • #2
By "equivalent logic" you may mean "logically equivalent", that is, the formulas logically imply each other. But an appeal to semantics defeats the purpose of proving that a formula is a theorem in a formal system. For this you need a derivation.

Next, system K (Hilbert system) is almost impossible to use for building proofs (though it is easy to prove things about it), at least until a significant number of metatheorems, like the deduction theorem, is proved. You may be stuck if your course or book uses it, but I would recommend some version of natural deduction, which is much more user friendly. The metatheorems I talked about make Hilbert system more like natural deduction anyway.

Also, axioms you gave don't use the existential quantifier. Doe this mean that $\exists x\,A$ is a contraction for $\neg\forall x\,\neg A$? If so, one idea is to prove the contrapositive
\[
\neg\neg\forall x\,\neg A(x)\to\neg A(a)
\]
and then use K3. If you can derive $\forall x\,\neg A(x)$ from $\neg\neg\forall x\,\neg A(x)$, then you can just use K5.
 

1. What is logic?

Logic is the study of reasoning and argumentation. It involves evaluating the validity and soundness of arguments using principles and rules of inference.

2. What is a formal system?

A formal system is a set of symbols, rules, and axioms used to represent and manipulate mathematical or logical expressions. It provides a rigorous framework for proving theorems and making logical deductions.

3. What is the role of theorem proving in formal systems?

Theorem proving involves using the rules and axioms of a formal system to systematically derive new statements from existing ones. This allows us to prove the validity of a statement and establish its logical truth within the given system.

4. What is the K system in formal logic?

The K system, also known as the modal logic system K, is a formal system used to reason about necessity and possibility. It is based on the notion of possible worlds and is often used in philosophy, mathematics, and computer science.

5. How do you prove a theorem in formal system K?

To prove a theorem in formal system K, one must follow the rules of inference and use the axioms of the system to systematically derive the theorem from known statements. This requires a clear understanding of the system and its underlying principles.

Similar threads

  • Set Theory, Logic, Probability, Statistics
Replies
1
Views
2K
  • Set Theory, Logic, Probability, Statistics
Replies
2
Views
1K
  • Set Theory, Logic, Probability, Statistics
Replies
1
Views
1K
  • Set Theory, Logic, Probability, Statistics
Replies
1
Views
2K
  • Set Theory, Logic, Probability, Statistics
Replies
14
Views
3K
  • Set Theory, Logic, Probability, Statistics
Replies
1
Views
2K
  • Calculus and Beyond Homework Help
Replies
2
Views
2K
  • Set Theory, Logic, Probability, Statistics
Replies
5
Views
3K
  • Calculus and Beyond Homework Help
Replies
1
Views
2K
  • Math Proof Training and Practice
Replies
10
Views
1K
Back
Top