3
votes
2answers
80 views

If $T$ proves any incorrect $\forall$-rudimentary sentence, then $T$ is inconsistent

A theory $T$ in the language of arithmetic is called $\omega$-inconsistent if for some formula $F(x)$, $\exists x F(x)$ is a theorem of $T$, but so is $\neg F(n)$ for each natural number $n$. ...
3
votes
3answers
125 views

Trivial proof in ZFC

Let's take some theorem of ZFC, e.g.: $$(1)\: \exists x \forall y ( y \notin x) $$ We can then choose a constant, denote it by '$\varnothing$' to get the following: $$(2)\:\forall x (x\notin ...
1
vote
1answer
44 views

Prove the admissibility of $\Gamma, A \vdash_N B $, from $\Gamma \vdash_N B$

(This is an assignment) To prove: $$\frac{\Gamma \vdash_N B}{\Gamma, A \vdash_N B}$$ ($\Gamma, A = \Gamma \cup \{A\}$) I have what I think is a proof for this. I would like and be grateful for ...
2
votes
0answers
48 views

Certain sequents as inference rules

Fix a signature $\sigma.$ Then a coherent formula is a first-order formula built using only $\{\wedge,\vee,\top,\bot,\exists\}.$ See the link for more information. Furthermore, by a "special" ...
3
votes
2answers
63 views

Textbook on Basics of Formal Systems

Whilst trying to learn more about logic I came across Smullyan's Theory of Formal Systems on Google Books. What I liked about the book was how clearly it managed to describe (on pages 3-5 in chapter ...
1
vote
2answers
110 views

$\beta$ - conversion and $\alpha$-reduction problem in $\lambda$-calculus

Here is an expression that I am trying to reduce and my operations so far: $$((\lambda x.(x (\lambda z.zy))) (\lambda z.\lambda y. zy) )= (x (\lambda z.zy))[x \to \lambda z.\lambda y. zy ] = ...
0
votes
1answer
51 views

Is this $\beta$-reduction well defined?

Would it be possible to apply $(\lambda x.\lambda y. x)$ to the argument $y$? It seems to me that this must not be possible as it would give a different answer if applied to a constant, call it ...
3
votes
1answer
111 views

From a foundational point of view, what's a good specification language for formal systems?

Suppose you and I are writing a book that develops (classical) mathematics from scratch. In the course of writing this book, we'll need to define a variety of formal systems, like a system for ...
1
vote
1answer
54 views

In a string rewriting system, does rewriting consume the string?

In string rewriting system, does rewriting 'consume' the string? For instance, suppose $101$ is written down and there's a rule $1x1 \rightarrow 11x11,$ we can apply this rule to write down $11011,$ ...
8
votes
2answers
213 views

How do we derive new inference rules?

I've been toying with a system of inference rules for propositional logic. I can use the system to prove theorems; but my question is, can I use the system to obtain new inference rules? Here are the ...
4
votes
1answer
171 views

Understanding the syntactical completeness

A formal system is syntactically complete if for each sentence (closed formula) $\varphi$ either $\varphi$ or $\lnot \varphi$ is provable. A formal system is semantically complete if every ...
1
vote
3answers
100 views

Are PA and ZFC examples of logical systems?

Wikipedia says A logical system or, for short, logic, is a formal system together with a form of semantics, usually in the form of model-theoretic interpretation, which assigns truth values to ...
6
votes
2answers
184 views

Symbols and terminology for distinguishing derivability from sequents

First some definitions to make it clear what I'm talking about: A deductive system is a set $J$ of judgments together with a set $R$ of inference rules each of the form $$ j_0 \leftarrow j_1, ...
8
votes
1answer
158 views

Some different versions of completeness of a formal system, of a logic and of a theory

I have seen people talking about Gödel's complete theorems and Gödel's incomplete theorems on math.SE. I am curious what they are really about, so I try to understand the meaning of completeness ...
4
votes
3answers
322 views

Aftermath of the incompletness theorem proof

This is somewhat of a minor point about the incompletness theorem, but I'm always a little unsure: So one proves that there is a formula which is unprovable in the theory of consideration. Okay, at ...
1
vote
1answer
69 views

Satisfiability problem for FOL[<,R]

Let FOL[<,R] be the fragment of first-order logic enriched with two relational symbols < and R and the first-order axioms that say: < is a strict partial order and R is an irreflexive and ...
1
vote
1answer
144 views

Definition and meaning of “Proof Schema”, “Class Sign”

I'm a newbie in advanced mathematics, and I'm trying to understand Godel's theorem. I came across these two words which I couldn't understand clearly. "Proof Schema" and "Class-Sign" Can anybody ...
1
vote
1answer
242 views

Differences between the formal grammar, formation rules and automaton for a formal language

Added: A formal grammar is a set of formation rules for strings in a formal language. Formation rules are rules for describing which strings of symbols formed from the alphabet of a formal language ...
1
vote
1answer
116 views

How it is possible that sound system is inconsistent

We have some sound deduction system (every provable sentence is true), which has property of principle of explosion and some theory T described in that system. Lets assume that theory T is ...
2
votes
2answers
318 views

How it is posible that $\omega$-inconsistency does not lead to inconsistency

After wikipedia: Theory is $\omega$-inconsistent if, for some property P of natural numbers, T proves P(0), P(1), P(2), and so on (that is, for every standard natural number n, T proves that P(n) ...
2
votes
3answers
671 views

Hofstadter's TNT: b is a power of 2 - is my formula doing what it is supposed to?

If you've read Hofstadter's Gödel, Escher, Bach, you must have come across the problem of expressing 'b is a power of 2' in Typographical Number Theory. An alternative way to say this is that every ...
3
votes
2answers
230 views

How does a recursive definition fit into a formal proof?

I understand a proof as a series of statements that are either axioms or follow from previous statements by a small set of rules of inference. I understand a recursive definition to be something like ...
1
vote
0answers
69 views

Differential fields and rings

If one is to compute the derivative of $$ y=3x+2 $$ by $$ \frac{\mathrm{d}(3x+2)}{\mathrm{d} x} $$ Would I be working with differential fields? Since differential fields is a first-order ...
4
votes
1answer
130 views

Computing square roots and calculus

If one were to verify that $$ \sqrt{2} < 3 $$ would the underlying formalisation require a logic more expressive than first-order? Or, is FOL sufficient since real numbers can be formalised in ...
1
vote
1answer
209 views

Expressing P = NP as a first order formula

I want to express P = NP in a completely formal way. My first try: There exists an algorithm A and a polynomial bound p such that for all input i, A(i) = true iff i is a satisfiable formula and ...
1
vote
1answer
61 views

How to show that a set does not contain a specific string

If I have a set $S$ defined as the smallest set $S$ over an alphabet $A=\left\{ \star, \urcorner,(,), a_0,a_1, \dots \right\}$ ( $S\subseteq \cup_{k \in \mathbb{N}} A^k$) satisfying: $\bullet \ a_0, ...
1
vote
2answers
152 views

Informal Equivalents of Mathematica “Set” and “SetDelayed”

How would one distinguish between what is meant by Mathematica's "Set" and "SetDelayed" functions in informal mathematical notation? Is there a way to make this distinction any any reasonably standard ...
0
votes
1answer
57 views

Formulation of “significantly” close/far

I am writing a tech document and I would like to formulate "significantly" close/far. For example a certain suboptimal solution $x^{\dagger}$ is "significantly close" to the optimal solution $x^{*}$. ...
7
votes
1answer
750 views

Formal System and Formal Logical System

I was reading the Wikipedia article for Mathematical_logic. When reaching Formal_logical_systems, I was curious about its definition and clicked into its own article Logical_system, which redirected ...
1
vote
2answers
298 views

formal rules for avoiding bound/unbound variable problems in lambda calculus

I have been interested in learning formal math formally enough so that I could write a proof assistant using some simple parsing tools, and explain to someone else with little math knowledge how to ...
9
votes
5answers
950 views

Resources for learning formal math?

I'd like to learn formal math. Preferably, though not necessarily, starting with predicate logic/first order logic rather than higher order logic. I am trying to find resources (papers, books etc.) ...
8
votes
1answer
857 views

The Power of Lambda Calculi

A simple question here, which likely demands a somewhat complex answer... Or rather, a set of related questions. What are the advantages of typed lambda calculus over untyped lambda calculus in ...