Semi-decidable means that will accept all correct formulas, and either rejects incorrect formulas or gives no answer. It's the same as having a generator that generates every correct formula eventually.
In my opinion, OP is incorrect and those systems are sound but indecidable.
> Semi-decidable means that will accept all correct formulas, and either rejects incorrect formulas or gives no answer.
By this definition, program incorrectness isn't semidecidable either - the compiler will accept all correct [incorrect] formulas, and will either reject or accept incorrect [correct] formulas.
Not really, because for undecidable problems semidecidability can only hold one-way. If it held in both ways then the language would be decidable.
Take the Halting program for example: For a program p which halts, you can determine whether it will halt in finite time (because by definition it halts). However, there is no semidecidable algorithm for "this program runs infinitely long".
I don't understand what you're trying to say. What are you contradicting with "Not really"? The claim above you is "by this definition, program incorrectness isn't semidecidable either". You're saying that it is?
In my opinion, OP is incorrect and those systems are sound but indecidable.