A formal system is broadly defined as any well-defined system of abstract thought based on the model of mathematics. (Def: http://en.m.wikipedia.org/wiki/Formal_system)

learn more… | top users | synonyms

0
votes
0answers
16 views

Second-order formulation of the Peano axioms

The Peano axioms in Peano's original formulation have an induction axiom (axiom 9) which quantifies over sets: If $K$ is a set such that: $0$ is in $K$, and for every natural number $n$, ...
1
vote
1answer
37 views

Loops in Robinson arithmetic

In the Robinson arithmetic, I wonder how the recursive definition of addition and multiplication can be well-defined. Axiom 3 seems to prohibit other chains starting with an element which has no ...
3
votes
2answers
41 views

Which functions can be obtained by applying these syntactic rules?

Here's an intentionally weird question for ye all. Start off with the expression $x$. Rule 0. We're allowed get a new expression from an old expression by replacing a subexpression with an $\mathbb{...
1
vote
3answers
72 views

What does “consistency” mean if formal systems are inherently meaningless?

In the book Gödel's Proof by Ernest Nagel and James R. Newman, the authors insist that formal systems are to be considered as meaningless mechanical systems, which yield theorems by merely applying ...
4
votes
0answers
82 views

The monadic second order theory with $<$ and Presburger arithmetic

Consider the monadic second order logic over the natural numbers with $<$ as a predicate, i.e. the second order logic over $(\mathbb N, 1, <)$, where we can quantify over sets and individual ...
5
votes
2answers
83 views

Formal systems in which $\forall x \in \mathbb{R}(x \neq 0 \rightarrow x^{-1} \neq 0)$ is true, but the contrapositive is disallowed.

Question. Are there any formal systems out there for which $$\forall x \in \mathbb{R}(x \neq 0 \rightarrow x^{-1} \neq 0)$$ is true, but the contrapositive $$\forall x \in \mathbb{R}(x^{-1} =...
4
votes
4answers
198 views

Calculus of Natural Deduction That Works for Empty Structures

Currently, I am dealing with the calculus of natural deduction by Gentzen. This calculus gives us rules to manipulate so-called sequents. Definition. If $\Gamma$ is a set of formulas and $\phi$ a ...
1
vote
4answers
108 views

natural deduction: introduction of universal quantifier and elimination of existential quantifier explained

Currently, I am dealing with the calculus of natural deduction by Gentzen. This calculus gives us rules to manipulate so-called sequents. Definition. If $\phi_1,\dots, \phi_n,\phi$ are formulas, then ...
0
votes
1answer
79 views

Is there any System that's not logicist?

I have this assignment about different types of formal logic systems, like Lewis S5, Fuzzy Logic and some others, but now they ask me to search for any non logicist system, but I've search a lot and ...
27
votes
9answers
2k views

Is formal truth in mathematical logic a generalization of everyday, intuitive truth?

I'm trying to wrap my head around the relationship between truth in formal logic, as the value a formal expression can take on, as opposed to commonplace notions of truth. Personal background: When I ...
1
vote
1answer
49 views

What formal systems are various programming paradigms based on?

I heard that functional programming paradigm is based on lambda calculus and combinatory logic. If I am correct, lambda calculus and combinatory logic are formal systems. What formal systems are ...
1
vote
0answers
32 views

What is the root of first class object in programming languages?

What is the root of "first class object" of programming languages? (Also see https://en.wikipedia.org/wiki/First-class_function, and http://stackoverflow.com/questions/245192/what-are-first-class-...
2
votes
1answer
40 views

Are these results generalizable?

It is a well-known fact that Euclidean geometry and the arithmetic of real numbers are both decidable and complete theories. Here are my questions: Do the non-Euclidean geometries share the same ...
6
votes
3answers
247 views

Why is establishing absolute consistency of ZFC impossible?

Why is establishing the absolute consistency of ZFC impossible? What are the fundamental limitations that prohibit us with coming up with a proof? EDIT: This post seems to make the most sense. In ...
3
votes
1answer
92 views

Why can't we keep adding axioms forever?

Let F be a formal system falling prey to Gödel's incompleteness theorems, implyng there is a true but unprovable statement, call it $G_1$. Of course, adding $G_1$ to the axioms of F doesn't solve the ...
0
votes
0answers
22 views

Can there be true but unprovable statements about object other than numbers?

In ZFC, everything is a pure set, and because the necessary amount of arithmetic for the Gödel's incompleteness theorems to go through is interpretable within ZFC, there are undecidable statements ...
0
votes
2answers
54 views

Impossibility of proving a foundation to be consistent

An argument came to my mind that seems really mind-blowing and I haven't found it anywhere. Here's how it goes: We call a formal system F embodied in classical logic a foundation of mathematics when ...
2
votes
0answers
39 views

Why is \mathsf{} used for formal systems?

A lot of times I have seen well-respected members of this community edit posts (including mine) changing things like "ZFC" into "$\mathsf{ZFC}$". It kind of makes sense, because formal systems like ...
0
votes
0answers
25 views

Simplest way to say “$\varphi$ is a wff of formal system $\mathbf{F}$”?

What is the simplest way to say "$\varphi$ is a well-formed formula of formal system $\mathbf{F}$" in symbols? The only thing that comes to mind is: $$\varphi \in \mathbf{F}$$ Am I right? I.e., ...
0
votes
1answer
35 views

Any foundational theory of math falls prey to the incompleteness theorems - true or false?

I heard somewhere on the internet once something along the following lines: Any conceivable foundational theory of mathematics (be it ZFC or, if ZFC was found to be inconsistent, some modification ...
3
votes
1answer
59 views

What is the simplest formal system falling prey to Gödel's incompleteness theorems?

What is the the simplest formal system falling prey to Gödel's incompleteness theorems? Is the answer different for the first and second theorems? Is the answer Q for the first theorem and PRA for ...
0
votes
0answers
11 views

Metamathematic: Cover the case if X=Y

I want to formalize: "If X is less than Y, Then U is equal to Y ", and have been told that $$ \bf [\forall V \sim X=(Y+V)]U=Y $$ does not cover the case X=Y. Therefore I have rewritten it as $$ \bf [\...
5
votes
0answers
92 views

Is it possible to formalize all mathematics in terms of ordinals only?

Our experience shows that all finitary mathematical objects could be encoded using the natural numbers, and all operations on those objects could be expressed in terms of a few basic operations on ...
1
vote
0answers
14 views

Can I effeciently check whether the inverse of a semantic function exists?

I'm relatively new to the fields of formal semantics/systems/languages or even model theory and therefore I miss some knowledge and experience. I try to boil the question down to the core essence of ...
0
votes
0answers
37 views

Algebraic embeddings and isomorphisms in formalized ZFC

Example: It is always said that we can embed $\mathbb{Z}$ within $\mathbb{Q}$ by identifying $z \in \mathbb{Z}$ as $(z,1) \in \mathbb{Q}$. This is because there is an injective ring homomorphism $\phi ...
0
votes
1answer
25 views

Given a formal system show that a variable contains more of one symbol than an initial part of that variable

Given a formal system[of 4 symbols: 0, 1, ( , ) ] with rules: You may write down 0 or 1 at any time. if strings s and t have been written down, you may write down (st). write ⊢s to mean that s can ...
1
vote
1answer
59 views

Recursive definitions in formal logic

A binary tree $T$ is either A single vertex, or A graph formed by taking two binary trees, adding a vertex, and adding an edge directed from the new vertex to the root of each binary tree. Suppose ...
1
vote
1answer
73 views

Is there a definition of the existential quantifier which does not imply the axiom of choice?

The definition of the existential quantifer given in Bourbaki's Theory of Sets is $$(\exists x)R \iff (\tau_x(R)\mid x)R.$$ Here $x$ is a letter, $R$ is a relation, and $(\tau_x(R)\mid x)R$ means ...
0
votes
2answers
75 views

How can Godel's theorem apply to every formal system?

How can Godel's theorem apply to any formal system of logic, if the truth of the theorem itself is only relative to the axioms and rule of inference that were used to generate it. In other words ...
1
vote
2answers
105 views

Analysis and formal proofs.

Ever since I started learning formal logic I've had these kind of doubts: Is analysis ever studied in a completely axiomatic/formal proofy way? What I mean is, given a set of axioms and inference ...
1
vote
2answers
39 views

Peano Arithmetic: How would this formalized statement be correct?

Using Peano Axioms I have formalized the following: x is the square of an odd prime number For some odd prime number x' , x is its square IF x is some odd prime number, THEN x is the square of x' IF ...
0
votes
0answers
47 views

Do we use Z specification language these days?

I am studying organization and properties of CAM (Content Addressable Memory) of a network switch. While searching for applications of Z, I found that there are several formalization projects ...
2
votes
0answers
50 views

Connection between Algebraic structures and Formal Systems

I am a college student with very little mathematics background (up to Calculus 152 at Rutgers University), but have become increasingly interested in computing and mathematics in the last year. I am ...
1
vote
2answers
107 views

Can there exist a definition of 'multiplication' in Presberger Arithmetic?

According to Wikipedia, Presberger Arithmetic is the first-order theory of the natural numbers with addition. It can be proved to be consistent, complete, and decidable. Though it contains no axioms ...
1
vote
1answer
64 views

What's wrong with this proof that ZFC is consistent

If we take ZFC minus all it's axioms, we can easily prove that ZFC's first axiom is independent (because all statements are independent in a formal system without any axioms). We can then prove that ...
1
vote
1answer
31 views

Will assuming an undecidable statement result in a consistent system?

If you assume that an undecidable statement in a consistent axiomatic system is true (or false), will that new system also be consistent? For example, does $\mathsf{ZF}$ being consistent imply that ...
0
votes
3answers
91 views

Rational numbers and leibniz law

Leibniz law says $a = b \implies f(a) = f(b)$. Unfortunately this law seems to fail for rational numbers e.g. ${1 \over 2} = {2 \over 4}$ but $numerator({1 \over 2}) \neq numerator({2 \over 4})$. I ...
0
votes
1answer
62 views

Order of Parentheses is Irrelevant: Metatheorem?

Here was shown by induction that the order of parentheses is irrelevant when associativity is verified. Question: Would this be a metatheorem about the formal language (say, of ZF) where the ...
0
votes
1answer
40 views

Is there a formal system which is generally accepted, and how is it called?

I read the question at Gödel's Incompleteness Theorem -- meta-reasoning "loophole"? about Gödel's incompleteness theorem. My question is little about the contents of that other ...
3
votes
2answers
82 views

Proving the rules of a complicated game are well defined

What strategy could one use to formally model a game and prove that the rules do not lead to any self contradiction? A major example that comes to mind is Magic the Gathering. The card ...
1
vote
0answers
27 views

Logical systems and formal proof

Is there any good book dealing with various formal systems and a book for formal proofs. Or atleast some good notes. This page on wikipedia also says: 'This article needs attention from an expert in ...
3
votes
0answers
83 views

What do the ZFC axioms look like in terms of subset?

I'm reasonably familiar with the ZFC axioms. I know they can be formalized in many different ways. However, I usually see them presented in terms of the elementary "propositional calculus primitives" $...
3
votes
1answer
62 views

Incompleteness of formal systems as opposed to completeness of a non-formal theory

I have read that Gödel's incompleteness theorem does not apply to real closed field theory. But the incompleteness theorem applies only to formal systems, that is systems whose alphabet of symbols and ...
0
votes
0answers
51 views

Strong logical system without principle of explosion

Are there some logical systems strong enough to contain theorems of first/second order Peano Arithmetic but constructed in such way that principle of explosion does not hold for them?
0
votes
1answer
119 views

Regular Expression of alternative 0's and 1's?

Let $L$ be the language of $0$'s and $1$'s in alternate positions, where $$ L = \{ \epsilon, 0, 1, 01, 10, 01010,\ldots\}. $$ Is $(0)*$ + $(1)*$ a valid regular expression that represents this ...
2
votes
1answer
214 views

Difference between Hilbert program and Russel & Whitehead's Principia Mathematica

May some one explain me what is difference between Hilbert program and Russel & Whitehead's Principia Mathematica? I know both of them wanted to reduce the mathematics into a set of axioms and ...
0
votes
1answer
50 views

prove this theorem $\vdash (\exists x_i (A\to B)\to (A\to \exists x_i B))$

Here is my thought to prove the theorem we should get $\{\exists x_i (A \to B), A\} \vdash \exists x_i B $ then, I don't know how to process...
0
votes
1answer
193 views

True or false? If $\eta$ is an explicitly defined incomputable number, then no formal system can pin down the value $\eta$ to arbitrary precision.

Let $\eta$ denote an explicitly defined incomputable real number (the bounty text is faulty, and does not mention incomputability of $\eta$). Then I think that no (recursively ennumerable) formal ...
2
votes
1answer
328 views

How can a proof by formula induction in a formal language be formalized?

From a set of not-so-rigorous lecture notes on Metalogic: Formulas of $L$: (i) Each sentence letter is a formula. (ii) If $A$ is a formula, then so is $\neg A$. (iii) If $A$ and $B$ ...
5
votes
3answers
129 views

Is there such a thing as the number of axioms?

This question was inspired by this question. Does it really make sense to say that a formal system has some number of axioms, say three, or ten, etc? E.g., take a formal system that admits ...