Is it possible to have logic without syntax (with only semantic proof methods)?

Question

In one paper I have read a note "Thus, unlike approaches which make use of full first order logic, unprovability of a formulae with respect to a agent specification can be shown by each of two approaches automatically without reliance on modeltheoretic consideration outside the actual proof method".

note means that there are proof methods that use semantic (model theoretic) and not syntactic means. Usually such situation can arise (and is the only possible way forward) when the logic under consideration does not have soundness and completeness properties.

The question is - are there semantic methods (or other non-syntactic methods) that can be used to prove some formulas of non-sound and/or non-complete logics. I can imagine in practice that this can mean the following: logic can have syntax and syntactical proof methods but those methods work for only part of formulae (e.g. for some syntactically specified fragments). If the proof of more complex formulae are required then semantic methods can be used. Such combined approach can be used in practice. So - is there described approach in reality?

p.s. Annals of Mathematics has article 'Proofs without syntax', it is about fact that different sturcutres can be used in place of formal languages - e.g. formal language can be substituted by graph structures. Actually I think that this not big achievement and it is still like having formal language. Semantics usually give far more opportunities than regulated syntactical structures.

Answer 1

I am not exactly sure if this is what you are looking for but a simple example could look like a propositional calculus where we remove modus ponens (the only inference rule) to get an incomplete system. In such system, given a sentence $\varphi$, one could "semantically prove" $\varphi$ to be true by exhibiting an exhaustive truth table.

Another example that might interest you is the question of whether two algebraic objects are isomorphic or not. If they are not isomorphic, one could try to show that one of the object satisfy some algebraic condition $A$ whereas the other doesn't. For instance, in group theory where the models of the theory are groups, one can show $\mathbb{Z}_4$ is not isomorphic to $\mathbb{Z}_2 \times \mathbb{Z}_2$ by showing that one is cyclic and the other is not. This could be interpreted as a "semantic" approach.

Answer 2

In the study of logic, there are two approaches. You can start with just logic and a few axioms, or you can start with the mathematics you like, and prove within it the validity of logical definitions (in particular, this approach gives reverse mathematics). You can read the introduction of the Cori-Lascar book for this complementarity.

Suppose you did not define any logic, but you have some semantical rules on some structures. Then you will be able to organize your semantic into a category, and then be able to reconstruct logic as the internal language of this category.

There are some paraconsistent logics and other alternatives that are used by some AI researchers to capture the behaviors of some of their programs where you need to rely on semantic methods; this is because 'ex falso quod libet', so to avoid proving everything these systems don't have cut elimination. These systems are fairly controversial for this reason.

In another direction, there's the grand programme of Jean-Yves Girard on the transcendental syntax, which aims to go beyond the tarskian syntax/semantic duality (i.e., there's 'and' and there's "'and'").

Transcendental syntax I: deterministic case I: deterministic case http://iml.univ-mrs.fr/~girard/trsy1.pdf