3
votes
1answer
99 views

What does “calculus” mean?

"calculus" and "formal system" From http://en.wikipedia.org/wiki/Propositional_calculus#Terminology a calculus is a formal system that consists of a set of syntactic expressions ...
0
votes
3answers
81 views

Are axioms assumed to be true in a formal system?

In a logical system, there is assignment of truth values to the sentences in the language, and axioms are assigned the true value. A logical system is a formal system. In a formal system, there is ...
4
votes
2answers
70 views

Are there formal systems that are not logical systems?

From WIkipedia 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 ...
0
votes
1answer
35 views

What do “completely described” and “complete formalisation” mean?

From Wikipedia In mathematics, an axiomatic system is any set of axioms from which some or all axioms can be used in conjunction to logically derive theorems. A mathematical theory consists of ...
2
votes
2answers
135 views

Precisely, what is a primitive recursive definition?

If I understand correctly, the language of primitive recursive arithmetic has a distinguished function symbol $S$, together with a function symbol for each primitive recursive definition (hereafter ...
3
votes
2answers
86 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$. ...
1
vote
1answer
49 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
56 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
94 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
142 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
56 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
112 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
234 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
195 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
102 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
197 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
176 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
335 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
148 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
268 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
119 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
354 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
757 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 ...
4
votes
2answers
247 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
70 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
132 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
211 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
153 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 ...
7
votes
1answer
883 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
311 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
1k 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
879 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 ...