A formal system comes with both a syntactic component, which determines the notion of provability ($\vdash$), and a semantic component, which determines the notion of truth ($\vDash$).
For this question assume that we don't know if $\vdash$ and $\vDash$ are equivalent.
What is the well-accepted definition of decidability of a system? I'm confused between the following two:
Decidable if for any formula $F$, there exists an algorithm to determine if $F$ is true
Decidable if for any formula $F$, there exists an algorithm to determine if $F$ is provable
Similarly for completeness I'm assuming it is defined as:
- Complete, if for every $F$, if $\vDash F$ then $\vdash F$