Recently I have been very fascinated by the claim and impact of Godel's incompleteness theorem. To understand the proof given by Godel, I felt the need to read an introductory book in logic to begin with. I have started reading the book titled "A Mathematical Introduction to Logic" by Herbert Enderton. As mentioned by the author, the aim of this book is to formalize the concept of: logical reasoning, truth, proof, etc. In the first chapter of this book the author introduces Sentential Logic. Further, to prove a few results in this chapter, the author provides proofs which are based on basic logical deductions.
My doubt is the following: Our aim of introducing sentential logic was to formalizing certain aspects of logical reasoning, however, in proving a few results about this new system (sentential logic) we use intuitive logic itself. But can we use a circular argument like this for proving?
Please let me know as to where my understanding about sentential logic lacks. I'm just starting with the field of mathematical logic and am currently stuck at this philosophical doubt, hence any help would be very welcome.
It would be circular if we're trying to prove the validity of our pre-theoretic logical reasoning, but it's not circular if we're just formalizing it—of course we can use our pre-theoretic reasoning to prove that our formal system matches our pre-theoretic reasoning!
Formalizing our pretheoretic reasoning doesn't itself tell us if our pretheoretic reasoning is in good order. We do, though, sometimes think that formal logic can tell us that our pretheoretic reasoning is not in good order—that a result in the formal system tells us we need to change some part of our pre-theoretic understanding. How can that happen if we used our pre-theoretic understanding to develop it?
As an example, consider what happened with naive set theory. We formalized (kind of) our pre-theoretic understanding of sets, and were using the same understanding to think about the system. Then Russell showed that the formal system allowed us to prove contradictions—and so if we had formalized everything right, there had to be something wrong with our pretheoretic understanding.
Similar things happen in logic. For example, it turns out that we can prove contradictions if we add a formalization of our pre-theoretic understanding of the truth predicate ("It's true that p.") to our system. The fact that we use pre-theoretic logical reasoning in developing these systems and proving metalogical results doesn't change the fact that there's now an inconsistency—you can think of it as essentially a reductio on our pretheoretic understanding, where we assumed it at the outset and then, by formalizing it, showed that it lead to contradiction.
If we take this as showing that we should get rid of some part of our pretheoretic reasoning, we would then have to look back over our metalogical proofs and get rid of it there too.
But in deciding what to get rid of—or even in thinking that a contradiction is a problem—we rely on other parts of our pretheoretic reasoning. Neurath had a nice metaphor for this sort of problem:
Like Mauro said, we can't possibly avoid using some pretheoretic logic in our development of the formal system—we can't stand in the sea while we reconstruct our ship. But we can stand on one part of our boat while working on another.
Similarly, we can use formal systems vindicate part of our pretheoretic reasoning relative to the part we're standing on. If we formalize some portion of our pre-theoretic reasoning and use a smaller part as our metalogic to prove consistency, etc., we could think of it as showing that the extra bit we formalized doesn't add any new problems not already in the smaller part.