Questions tagged [metalogic]

For questions related to metalogic. It is the study of the metatheory of logic. Whereas logic studies how logical systems can be used to construct valid and sound arguments, metalogic studies the properties of logical systems. Logic concerns the truths that may be derived using a logical system; metalogic concerns the truths that may be derived about the languages and systems that are used to express truths.

Filter by
Sorted by
Tagged with
2 votes
1 answer
115 views

Non-syntactic characterization of $\Delta_0$ formulae

A common schema in intuitionistic, constructive set theories is that of $\it{\Delta_0}$ separation: $$ \forall x\exists y\forall z(z\in y\leftrightarrow z\in x\wedge\phi(x, z))\text{ provided $\phi$ ...
Soundwave's user avatar
  • 423
0 votes
1 answer
50 views

How to prove that the set of theorems of any recursively axiomatized theory is a recursively enumerable set?

I read the article Craig's theorem written by Putnam (1965). I don't understand the claim on page 3 of the article: The set of theorems of $T$, where $T$ is any recursively axiomatized theory, is ...
유준상's user avatar
2 votes
2 answers
129 views

Meaning of "theorem of a system"

The following excerpt is from page 357 of Logic: The Laws of Truth by Nicholas Smith: Given a system of proof - say, the tree method for GPLI - we call propositions that can be proven using that ...
user51462's user avatar
  • 673
1 vote
2 answers
103 views

Proof of contraposition theorem using logical (semantic) entailment definition

I have been reading some older course material from Propositional Logic and I stumbled on a question, and I am unsure on how to start the proof. The question is: Prove the following theorem (...
Freyness's user avatar
2 votes
1 answer
150 views

Explain Godel's Second Incompleteness Theorem: Why is A Theory Unable to Prove its Consistency if it is Consistent?

From Peter Smith's Godel book (p. 6) "ConT" means "theory T is consistent" "GT" is "Godel unprovable sentence" ConT $\to$ GT inside T ...it immediately follows ...
Agapito Martinez's user avatar
2 votes
1 answer
77 views

Gödel's theorems, Löb's theorem, difference between "proves" and "implies"

Layman reading up on Gödel's theorems. I think I have some basic idea of how it all works in the abstract, but I'm still having a hard time distinguishing between (or even counting) the concepts ...
Quuxplusone's user avatar
1 vote
0 answers
34 views

Is it possible to axiomatize classical logic with only two meta-variables?

In the usual axiomatization of propositional logic with the $\to$ and $\lnot$ connectives, we have the modus ponens inference rule (from $p$ and $p \to q$ infer $q$) and the axiom schemes: $p \to (q \...
Cristian Gratie's user avatar
1 vote
2 answers
101 views

Is the deducutive apparatus of a formal system necessarily a set of inference rules?

In the book "Logic" by Paul Tomassi, the author uses the term deductive apparatus to refer to the set of inference rules in propositional logic and first-order logic. The use of this term ...
RyRy the Fly Guy's user avatar
0 votes
0 answers
29 views

Help in understanding this proof in Mendelson [duplicate]

Am new to Logic, and am having difficulty with this proof of Proposition 2.10 of Mendelson's Book "Introduction to Logic". The proposition describes a rule termed "Rule C", whereby ...
Link L's user avatar
  • 909
1 vote
0 answers
67 views

Not wanting to express the Gödel number of the actual string

Let's say I have a string of $n$ symbols, each with a Gödel number denoted $\ulcorner s_x \urcorner$, where the $x$ denotes that it is the $x$th symbol in the string. The Gödel number of the entire ...
user110391's user avatar
  • 1,057
0 votes
1 answer
45 views

Bisimulation games to compare equivalent but not bisimilar BML models

Two BML models M, w and N, w' are given: in M, w has with infinitely many R-transitions of finite length, and in N, w' has infinitely many R-transitions and also includes an infinite-length R-...
daci's user avatar
  • 1
0 votes
0 answers
121 views

What is the most primitive notion in mathematics?

I had a recent conversation with a professional mathematician about the status of relations, functions and predicates. I was arguing that it seems intuitive (to me at least) to classify them in this ...
Vivek Joshy's user avatar
2 votes
1 answer
84 views

Are there "Godel encodings" for non-arithmetic theories?

This is probably a very naive question, but is there something about Godel encoding that is essentially arithmetical, or is it possible to construct analogous mappings between the objects studied in a ...
Rando McRandom's user avatar
0 votes
0 answers
50 views

How to prove the Gödel sentence is true (in the metalanguage), assuming only consistency of a theory.

Let $T$ be a consistent, axiomatizable extension of $Q$ (Robinson or Minimal arithemthic shouldn't matter). We construct the Gödel sentence by using the diagonal lemma as: $\vdash_T G_T \...
Andrew Bayer's user avatar
2 votes
1 answer
164 views

Type Theory as a Meta-Language for Logic

I am unsure which StackExchange site is the most appropriate for this question, but I believe this site is the most appropriate. My current project involves rigorously proving all the mathematical ...
rfloc's user avatar
  • 961
1 vote
1 answer
127 views

Logical systems that are only weakly sound / weakly complete?

I understand the basic concepts of soundness and completeness in logical systems. However, when I took a look at the Wikipedia pages on both concepts, I saw that it listed a seperate strong form of ...
Nico's user avatar
  • 452
2 votes
0 answers
73 views

What if the metatheory is itself intuitionistic?

Usually, even in intuitionistic logic, the metatheory is classical. That is, to give just one example, either something is a theorem of intuitionistic logic, or it is not. That is an example of a ...
user107952's user avatar
  • 20.2k
0 votes
1 answer
86 views

Other important results of class/set distinction?

Most explanations of classes vs sets motivate the discussion via Russell's paradox. This feels like a kind of "gotcha technicality" to me, in the sense that one might reasonably prove ...
Him's user avatar
  • 447
5 votes
3 answers
271 views

Are there infinitely many metalogics?

Given the definitions of material implication, logical implication, and what a tautology is, we can prove: $$\mathcal B\text{ logically implies }\mathcal C\text{ if and only if }(\mathcal B\rightarrow\...
GDGDJKJ's user avatar
  • 864
0 votes
0 answers
78 views

Questions on metalogic and consistency

We know from Godel's theorems that interesting logics can not prove their own consistency, so whenever we want to prove the consistency of such a logic $L$, we need to take a step back, place this ...
Cristian Gratie's user avatar
5 votes
0 answers
119 views

Are soundness and completeness a part of proof theory, model theory or something else?

I have a question that I hope can clarify the scopes of model theory and proof theory. I have the following naïve understanding of the two areas (please correct me if I'm wrong): Model theory is ...
dumbo's user avatar
  • 71
2 votes
0 answers
83 views

Logical consequence (⊨ and ⊢) — A statement? A judgement? A meta-statement?

I'm trying to understand the terminology used in mathematical logic and I'm confused about the distinctions between statement, proposition, judgement, claim, and meta-variants of those. In particular, ...
dumbo's user avatar
  • 71
2 votes
1 answer
69 views

What types of axioms retain consistency of ZFC under additional axioms about its consistency?

My question is pretty simple. If ZFC does not prove that it is not consistent, then can we add the axiom to ZFC that it proves it is not consistent and is consistent and achieve equiconsistency? I ...
Eric sidenis's user avatar
4 votes
1 answer
190 views

What is the link between interpretability hierarchy and consistency strength

I am trying to understand this definition https://plato.stanford.edu/entries/independence-large-cardinals/#IntHie of Interpretability Hierarchy and how it relates to the concept of Consistency ...
Matteo Casarosa's user avatar
1 vote
0 answers
114 views

Is this style of proof clear and readable?

$\def\p {\phi} \def\P {\Phi} \def\q {\psi} \def\s {\vDash_{\tiny{PL}}} \def\ns {\nvDash_{\tiny{PL}}} \def\bigc #1{\vec\P_{#1}^\q} \def\pli {\mathscr{I}} \def\val #1{V_\pli(#1)} \def\mf {\p_1,\,\p_2,\,\...
Ten O'Four's user avatar
  • 1,056
0 votes
0 answers
286 views

Is this a valid way to prove the soundness of an inference rule in propositional logic?

I've been playing around with another proof and I'm wondering if it's an OK way to approach the proof? Is there some reason that it causes problems? All suggestions and thoughts are welcome. Proof ...
Ten O'Four's user avatar
  • 1,056
4 votes
1 answer
323 views

(Solution verification and criticism) If wff $\phi$ has no repetition of sentence letters, then $\nvDash \phi$

Edit: Here is attempt number 2. I've been much more terse, which I think flows much better. I've also changed the binary connective to disjunction to improve readability as well. By truth table $\lnot\...
Ten O'Four's user avatar
  • 1,056
4 votes
1 answer
97 views

Meta-Definition of Convergence

So, just recently I realized that the idea of convergence is not "all encompassing"... Let me explain. I thought that the topological definition of convergence was the most basic one in the ...
Davi Barreira's user avatar
1 vote
2 answers
311 views

Valid form and true premises makes an argument sound, but do 'premises' mean P, Q, R,... or 'what comprises the antecedent'?

Suppose we have an argument 'Disjunctive Syllogism' as below: $$P\lor Q \\{\sim}P \\∴Q.$$ which essentially means $$\big((P\lor Q)\; \&\; {\sim} P\big) \to Q.$$ Its truth table: row P Q P$\lor$Q ~...
Mojtaba Mohammadi's user avatar
3 votes
1 answer
170 views

Why isn't math proofs just a computer trial and error?

I already asked a similar question, but I recently began a course of Logic and it gave me not an answeat but a refination of my question, which I redefine here. My thinking is the following: Suppose ...
Alexandre Tourinho's user avatar
1 vote
1 answer
301 views

Can metalogic and model theory be formalized?

All of mathematics formulated using ZFC can be "formalized" in the sense that each statement could be translated into a logical string, and each proof can be translated into a formal proof. ...
WillG's user avatar
  • 6,469
2 votes
0 answers
129 views

Finitary reasoning and the distinction between mathematical and metamathematical theorems

Godel has argued that Skolem's finitism was responsible for his failure to prove completeness, despite having all the components of a proof. One can challenge this argument with the objection that ...
Mallik's user avatar
  • 511
0 votes
1 answer
66 views

Demonstrate a nondenumerable set of consistent extensions of $\mathbf{Q}$ that are pairwise inconsistent.

Given that for any $n \in \mathbb{N}$, there are $2^n$ consistent, axiomatizable extensions of $\mathbf{Q}$ that are pairwise inconsistent, show that there is a nondenumerable set of such consistent ...
clay's user avatar
  • 2,701
1 vote
0 answers
45 views

Show a model of $\mathbf{Q}$ where this is false $\forall x \forall y (x \cdot y = y \cdot x) $

Show that there are models of $\mathbf{Q}$ where the following sentence is false \begin{align*} \forall x \forall y (x \cdot y = y \cdot x) \\ \end{align*} For reference, the ten finite axioms of $\...
clay's user avatar
  • 2,701
0 votes
1 answer
90 views

Prove that the minimal finitely axiomatizable theory of arithmetic $\mathbf{Q}$ plus the Rosser sentence is consistent.

Let $T$ be $\mathbf{Q}$ (which is a minimal finitely axiomatized theory of arithmetic). Let $R$ be the Rosser sentence of $T$. Let $T_0$ be $T + \{R \}$ and $T_1$ be $T + \{\sim R\}$. Show that $T_0$ ...
clay's user avatar
  • 2,701
0 votes
1 answer
59 views

Godel's first Incompleteness Theorem: Truth vs Derivability/Consequence

Consider some theory $T$ that is a consistent, axiomatizable extension of $\mathbf{Q}$. By the first incompleteness theorem, $T$ is incomplete, which means there is some true sentence $A$ that is not ...
clay's user avatar
  • 2,701
1 vote
1 answer
98 views

Computability and Logic by Boolos et all Problem 17.1

Show that the existence of a semirecursive set that is not recursive implies that any consistent, axiomatizable extension of $\mathbf{Q}$ fails to prove some correct $\forall$-rudimentary sentence. ...
clay's user avatar
  • 2,701
1 vote
1 answer
46 views

Understanding Textbook Proof: if theory $T$ is $\omega$-consistent, then if $\vdash_T \text{Prv}(\ulcorner A \urcorner)$ then $\vdash_T A$

Prove if theory $T$ is an axiomatizable $\omega$-consistent extension of $\mathbf{Q}$, then if $\vdash_T \text{Prv}(\ulcorner A \urcorner)$ then $\vdash_T A$ This is a textbook proof in Computability ...
clay's user avatar
  • 2,701
0 votes
1 answer
89 views

Problem 17.2 from Computability and Logic By Boolos et all

Let $T$ be a consistent axiomatizable theory extending $\mathbf{Q}$. Let $P^+$ be the set of (code numbers for) sentences provable from $T$; let $P^-$ be the set of (code numbers for) sentences ...
clay's user avatar
  • 2,701
2 votes
0 answers
123 views

deductive system where the axioms are all the propositions that are not tautology

let D be a deductive system. The system's axiom set, A, includes all propositions that are not tautology, and the only rule of inference is $\frac{\alpha \vee \beta}{\alpha \wedge \beta}$. I need to ...
CforLinux 's user avatar
0 votes
1 answer
128 views

Show that PA has a denumerable model that is not isomorphic to N

I know that PA has inifnitely many models that can satisfy itself, but how we do prove that it has one particular denumerable model that is not isomorphic to its standard interpretation N?
Cherry Blossom Bomb's user avatar
2 votes
2 answers
356 views

Show that the compactness theorem does not apply to infinite logic

I am trying to understand why the compactness theorem does not apply in infinite logic and I wonder if anyone has a good example and explanation for this? Edit: By infinite logic I mean logic that ...
idlatva's user avatar
  • 153
1 vote
2 answers
137 views

Prove that if two theories have the same countably infinite models, then they have the same models of each infinite cardinality.

I want to prove the following statement: Let $\Gamma_1$ and $\Gamma_2$ be two theories formulated in a countable language. Show that if $\Gamma_1$ and $\Gamma_2$ have the same countably infinite ...
idlatva's user avatar
  • 153
0 votes
1 answer
119 views

Consequence of Löwenheim-Skolem theorem

I am trying to understand the following consequence of Löwenheim-Skolems theorem: Let ∑ be a set of sentences in a countable language. If ∑ has any model, then it has a countable model. I do not ...
idlatva's user avatar
  • 153
0 votes
1 answer
147 views

Show that gamma has a model if and only if each set in gamma has a model

Let $\Gamma$ be a theory that is closed under provability. That is, if there are sentences $\varphi_{1},...,\varphi_{n}$ in $\Gamma$ such that $\varphi_{1},...,\varphi_{n} \vdash \phi$ it applies ...
idlatva's user avatar
  • 153
3 votes
3 answers
146 views

Intuition behind structural weakening

According to the Fitch deductive system I'm using in my logic class, the following is a valid inference: Premise: Q Step 1: Assume P Step 2: Q by reiteration Step 3: P → Q by conditional intro. ...
Joa's user avatar
  • 405
0 votes
1 answer
86 views

How to show that the intersection of two elementary classes is a elementary class

I am wondering how I can show that the intersection between two elementary classes is a elementary class. I have two elementary classes A and B, $A,B = (M|M\models\Gamma)$ and I want to give a proof ...
user15415514's user avatar
0 votes
1 answer
58 views

Do some rules of syntax permit a sentence to literally be an element of a set?

In meta-logic, it's routine to consider sets of sentences. However, are there rules of syntax that permit a sentence to be literally an element of a set? Is there always an explicit or implicit ...
Ren Eh Daycart's user avatar
4 votes
1 answer
298 views

In what formal system is Godel's Incompleteness Theorem (or similar statements of undecidability) proven?

For example, consider the proof using Rosser's trick as shown on wikipedia. https://en.wikipedia.org/wiki/Rosser%27s_trick#The_Rosser_sentence That proof isn't inside the arithmetical theory T, but in ...
Hank Igoe's user avatar
  • 1,408
2 votes
1 answer
1k views

What is the difference between $\leftrightarrow$, $\iff$, and $\equiv$, especially when used in the same text? [duplicate]

I think that the difference has something to do with object language and meta language, but I'm not sure. I've heard that $\leftrightarrow$ is a connective on a proposition level, whereas $\iff$ is a ...
NilsK's user avatar
  • 219